Added decision preferences of unseen terms

Author: Tomaqa

src/api/MainSolver.cc

@@ -162,23 +162,35 @@ void MainSolver::resetDecisionPreferences() {
     smt_solver->clearUserBranchLits();
 }
 
-void MainSolver::propagateDecisionPreferenceToSMTSolver(PTRef pref) {
+void MainSolver::propagateDecisionPreferenceToSMTSolver(PTRef pref, FrameId frameId) {
     assert(logic.getSortRef(pref) == logic.getSort_bool());
     assert(not logic.isConstant(pref));
 
-    Lit l;
-    if (logic.isBoolVarLit(pref)) {
-        l = term_mapper->getOrCreateLit(pref);
-        Var v = var(l);
-        smt_solver->addVar(v);
-    } else {
-        // Ignores substitutions ..
-        assert(term_mapper->hasLit(pref));
-        l = term_mapper->getLit(pref);
-    }
-    assert(term_mapper->getLit(pref) == l);
-    assert(term_mapper->getVar(pref) == var(l));
-    smt_solver->pushUserBranchLit(l);
+    // Ignores substitutions ..
+    Lit lit = [&] {
+        if (term_mapper->hasLit(pref)) { return term_mapper->getLit(pref); }
+
+        if (logic.isBoolVarLit(pref)) {
+            Lit l = term_mapper->getOrCreateLit(pref);
+            Var v = var(l);
+            smt_solver->addVar(v);
+            assert(term_mapper->getLit(pref) == l);
+            assert(term_mapper->getVar(pref) == var(l));
+            return l;
+        }
+
+        auto name = std::string{"pref"} + std::to_string(smt_solver->userBranchLitsSize());
+        PTRef decisionVarTerm = logic.mkBoolVar(name.c_str());
+        Lit l = term_mapper->getOrCreateLit(decisionVarTerm);
+        PTRef condTerm = logic.mkImpl(decisionVarTerm, pref);
+        sstat status = giveToSolver(condTerm, frameId);
+        assert(status == s_Undef);
+        assert(term_mapper->getLit(decisionVarTerm) == l);
+        assert(term_mapper->getVar(decisionVarTerm) == var(l));
+        return l;
+    }();
+
+    smt_solver->pushUserBranchLit(lit);
 }
 
 sstat MainSolver::simplifyFormulas() {
@@ -235,7 +247,7 @@ sstat MainSolver::simplifyFormulas() {
         }
 
         for (PTRef pref : decisionPreferences.scope(i)) {
-            propagateDecisionPreferenceToSMTSolver(pref);
+            propagateDecisionPreferenceToSMTSolver(pref, frames[i].getId());
         }
     }
     if (status == s_False) {
@@ -355,16 +367,17 @@ std::unique_ptr<InterpolationContext> MainSolver::getInterpolationContext() {
 }
 
 sstat MainSolver::giveToSolver(PTRef root, FrameId push_id) {
-
     struct ClauseCallBack : public Cnfizer::ClauseCallBack {
         std::vector<vec<Lit>> clauses;
         void operator()(vec<Lit> && c) override { clauses.push_back(std::move(c)); }
     };
+
     ClauseCallBack callBack;
     ts.setClauseCallBack(&callBack);
     ts.Cnfizer::cnfize(root, push_id);
     bool const keepPartitionsSeparate = trackPartitions();
-    Lit frameLit = push_id == 0 ? Lit{} : term_mapper->getOrCreateLit(frameTerms[push_id]);
+    Lit frameLit;
+    if (push_id != 0) { frameLit = term_mapper->getOrCreateLit(frameTerms[push_id]); }
     int partitionIndex = keepPartitionsSeparate ? pmanager.getPartitionIndex(root) : -1;
     for (auto & clause : callBack.clauses) {
         if (push_id != 0) { clause.push(frameLit); }

src/api/MainSolver.h

@@ -295,7 +295,7 @@ class MainSolver {
 
     inline bool trackPartitions() const;
 
-    void propagateDecisionPreferenceToSMTSolver(PTRef);
+    void propagateDecisionPreferenceToSMTSolver(PTRef, FrameId);
 
     PTRef rewriteMaxArity(PTRef root);
 

test/unit/test_DecisionPreference.cc

@@ -47,18 +47,21 @@ class DecisionPreferenceTest : public ::testing::Test {
         auto model = mainSolver.getModel();
         PTRef val_a = model->evaluate(a);
         PTRef val_b = model->evaluate(b);
+        assert(val_a != PTRef_Undef);
+        assert(val_b != PTRef_Undef);
         PTRef exp_val_a = lboolValToPTRef(expValA);
         PTRef exp_val_b = lboolValToPTRef(expValB);
-        EXPECT_EQ(val_a, exp_val_a);
-        EXPECT_EQ(val_b, exp_val_b);
+        if (exp_val_a != PTRef_Undef) { EXPECT_EQ(val_a, exp_val_a); }
+        if (exp_val_b != PTRef_Undef) { EXPECT_EQ(val_b, exp_val_b); }
     }
 
 protected:
     PTRef lboolValToPTRef(lbool val) const {
         auto & logic = osmt->getLogic();
         if (val == l_False) { return logic.getTerm_false(); }
         if (val == l_True) { return logic.getTerm_true(); }
-        return logic.getDefaultValuePTRef(logic.getSort_bool());
+        // return logic.getDefaultValuePTRef(logic.getSort_bool());
+        return PTRef_Undef;
     }
 
     std::shared_ptr<Opensmt> osmt{};