Merge branch 'development' into master

Author: ValentinPromies

CMakeLists.txt

@@ -15,7 +15,7 @@ include(smtratmacros)
 
 set(PROJECT_FULLNAME "SMT-RAT")
 set(PROJECT_DESCRIPTION "Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving")
-set_version(25 06)
+set_version(25 11)
 
 # set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/bin")
 set(EXECUTABLE_OUTPUT_PATH ${PROJECT_BINARY_DIR} CACHE PATH "Directory for built executables")

src/smtrat-modules/SATModule/SATModule.h

@@ -67,7 +67,8 @@ namespace smtrat
         //template<int num, int num2> friend struct VarSchedulingMcsatLowerFirstPerLevel;
         friend class VarSchedulerBase;
         friend class VarSchedulerMcsatBase;
-
+        template<mcsat::VariableOrdering vot>
+        friend class TheoryVarSchedulerStatic;
         private:
 
             /**

src/smtrat-modules/SATModule/mcsat/MCSATMixin.h

@@ -684,6 +684,11 @@ class MCSATMixin {
 		return *mVarPropertyCache[v].theoryVars;
 	}
 
+    public:
+    const std::map<Minisat::Var, std::vector<Minisat::Var>>& varDeps() const {
+        return mVarDeps;
+    }
+
 	// ***** Output
 	/// Prints a single clause
 	void printClause(std::ostream& os, Minisat::CRef clause) const;

src/smtrat-modules/SATModule/mcsat/VarSchedulerMcsat.h

@@ -40,12 +40,14 @@ namespace smtrat {
         std::vector<Minisat::Var> ordering;
         std::vector<Minisat::Var>::const_iterator nextTheoryVar = ordering.end();
         bool initialized = false;
+        const std::map<Minisat::Var, std::vector<Minisat::Var>>& varDeps;
 
     public:
 
         template<typename BaseModule>
         explicit TheoryVarSchedulerStatic( BaseModule& baseModule ) :
-            VarSchedulerMcsatBase(baseModule)
+            VarSchedulerMcsatBase(baseModule),
+            varDeps(baseModule.mMCSAT.varDeps())
         {}
 
         void insert(Minisat::Var var) {
@@ -86,6 +88,28 @@ namespace smtrat {
             std::cout << "Theory variable ordering: " << ordering << std::endl;
         }
 
+
+        // compare variables based on dependencies in the baseModule.
+        // l < r if r depends on l (possibly by transitive dependencies)
+        struct cmp_dep {
+            const std::map<Minisat::Var, std::vector<Minisat::Var>>& varDeps;
+            cmp_dep(const std::map<Minisat::Var, std::vector<Minisat::Var>>& vd) : varDeps(vd) {}
+
+            inline bool operator() (const Minisat::Var l, const Minisat::Var r) const {
+                auto it = varDeps.find(r);
+                if (it != varDeps.end()) {
+                    const auto& deps = it->second;
+                    auto it_l = std::find(deps.begin(), deps.end(), l);
+                    if (it_l != deps.end()) return true;
+                    return std::any_of(
+                        deps.begin(), deps.end(),
+                        [this, l](const auto& v){return (*this)(l,v);}
+                    );
+                }
+                return false;
+            }
+        };
+
         template<typename Constraints>
         void rebuildTheoryVars(const Constraints& c) {
             assert(!initialized);
@@ -96,6 +120,10 @@ namespace smtrat {
             for (const auto& tvar : tordering) {
                 ordering.push_back(minisatVar(tvar));
             }
+
+            // make sure dependencies are in the right order
+            std::stable_sort(ordering.begin(), ordering.end(), cmp_dep(varDeps));
+          
             nextTheoryVar = ordering.begin();
             initialized = true;
         }

src/smtrat-strategies/strategies/Default.h

@@ -117,8 +117,31 @@ class Default : public Manager {
                 addBackend<STropModule<STropSettings3>>({
                     addBackend<SATModule<SATSettingsMCSATApxVSIDS>>().condition(&condition_qf_nra_with_bool),
                     addBackend<SATModule<SATSettingsMCSATApxStaticTheory>>().condition(&condition_qf_nra_without_bool)
-                }).condition( &condition_nra ),
-                // QF_NIRA
+                })
+            }).condition( &condition_qf_nra ),
+
+            // QF_NRA extended with root expressions
+            addBackend<SATModule<SATSettingsMCSATApxVSIDS>>(
+            ).condition( &condition_qf_ra_ext ),
+
+            // NRA
+            addBackend<PNFerModule>({
+                addBackend<CoveringNGModule<CoveringNGSettingsDefault>>( // covering for quantifiers
+                ).condition( &condition_non_quantifier_free ),
+                addBackend<FPPModule<FPPSettings1>>({ // default QF_NRA solver
+                    addBackend<STropModule<STropSettings3>>({
+                        addBackend<SATModule<SATSettingsMCSATApxVSIDS>>().condition(&condition_qf_nra_with_bool),
+                        addBackend<SATModule<SATSettingsMCSATApxStaticTheory>>().condition(&condition_qf_nra_without_bool)
+                    })
+                }).condition( &condition_quantifier_free )
+            }).condition( &condition_nonqf_ra ),
+
+            // NRA  extended with root expressions
+            addBackend<CoveringNGModule<CoveringNGSettingsDefault>>(
+            ).condition( &condition_ra_ext ),
+
+            // QF_NIRA
+            addBackend<FPPModule<FPPSettings1>>({
                 addBackend<IncWidthModule<IncWidthSettings1>>({
                     addBackend<IntBlastModule<IntBlastSettings2>>({
                         addBackend<SATModule<SATSettings1>>({
@@ -146,25 +169,6 @@ class Default : public Manager {
                     addBackend<LRAModule<LRASettings1>>()
                 }).condition( &condition_lira_non_conj )
             }).condition( &condition_qf_base ),
-
-
-            // QF_NRA extended with root expressions
-            addBackend<SATModule<SATSettingsMCSATStaticTheory>>().condition( &condition_qf_ra_ext ),
-
-            // NRA
-            addBackend<PNFerModule>({
-                addBackend<CoveringNGModule<CoveringNGSettingsDefault>>( // covering for quantifiers
-                ).condition( &condition_non_quantifier_free ),
-                addBackend<FPPModule<FPPSettings1>>({ // default QF_NRA solver
-                    addBackend<STropModule<STropSettings3>>({
-                        addBackend<SATModule<SATSettingsMCSATApxVSIDS>>().condition(&condition_qf_nra_with_bool),
-                        addBackend<SATModule<SATSettingsMCSATApxStaticTheory>>().condition(&condition_qf_nra_without_bool)
-                    })
-                }).condition( &condition_quantifier_free )
-            }).condition( &condition_nonqf_ra ),
-
-            // NRA  extended with root expressions
-            addBackend<CoveringNGModule<CoveringNGSettingsDefault>>().condition( &condition_ra_ext ),
         });
     }
 };