Preprocessing decision preferences

Author: Tomaqa

src/api/MainSolver.cc

@@ -184,7 +184,7 @@ sstat MainSolver::simplifyFormulas() {
         if (status == s_False) { break; }
 
         for (PTRef pref : decisionPreferences.scope(i)) {
-            giveDecisionPreferenceToSMTSolver(pref, frameId);
+            giveDecisionPreferenceToSMTSolver(pref, frameId, context);
         }
     }
 
@@ -346,15 +346,15 @@ PTRef MainSolver::rewriteMaxArity(PTRef root) {
     return opensmt::rewriteMaxArityClassic(logic, root);
 }
 
-void MainSolver::giveDecisionPreferenceToSMTSolver(PTRef pref, FrameId frameId) {
+void MainSolver::giveDecisionPreferenceToSMTSolver(PTRef pref, FrameId frameId, PreprocessingContext const & pcontext) {
     assert(logic.getSortRef(pref) == logic.getSort_bool());
     assert(not logic.isConstant(pref));
 
     // Ignores substitutions ..
     Lit l = [&] {
         if (term_mapper->hasLit(pref)) { return giveExistingDecisionPreferenceToSMTSolver(pref); }
         if (logic.isBoolVarLiteral(pref)) { return giveBoolVarDecisionPreferenceToSMTSolver(pref); }
-        return giveAnyDecisionPreferenceToSMTSolver(pref, frameId);
+        return giveAnyDecisionPreferenceToSMTSolver(pref, frameId, pcontext);
     }();
 
     smt_solver->pushUserBranchLit(l);
@@ -380,17 +380,25 @@ Lit MainSolver::giveBoolVarDecisionPreferenceToSMTSolver(PTRef pref) {
     return l;
 }
 
-Lit MainSolver::giveAnyDecisionPreferenceToSMTSolver(PTRef pref, FrameId frameId) {
+Lit MainSolver::giveAnyDecisionPreferenceToSMTSolver(PTRef pref, FrameId frameId,
+                                                     PreprocessingContext const & pcontext) {
     assert(not term_mapper->hasLit(pref));
     assert(not logic.isBoolVarLiteral(pref));
 
+    // Cannot preprocess pref unconditionally - may result in a conflict
+
     auto name = std::string{".pref"} + std::to_string(pref.x);
     PTRef decisionVarTerm = logic.mkBoolVar(name.c_str());
     Lit l = term_mapper->getOrCreateLit(decisionVarTerm);
     PTRef condTerm = logic.mkImpl(decisionVarTerm, pref);
+    PTRef processed = preprocessFormula(condTerm, pcontext);
+    assert(not logic.isConstant(processed));
+    assert(not logic.isBoolVarLiteral(processed));
+
     [[maybe_unused]]
-    sstat status = giveToSolver(condTerm, frameId);
+    sstat status = giveToSolver(processed, frameId);
     assert(status == s_Undef);
+
     assert(term_mapper->getLit(decisionVarTerm) == l);
     assert(term_mapper->getVar(decisionVarTerm) == var(l));
 

src/api/MainSolver.h

@@ -307,10 +307,10 @@ class MainSolver {
 
     PTRef rewriteMaxArity(PTRef root);
 
-    void giveDecisionPreferenceToSMTSolver(PTRef, FrameId);
+    void giveDecisionPreferenceToSMTSolver(PTRef, FrameId, PreprocessingContext const &);
     Lit giveExistingDecisionPreferenceToSMTSolver(PTRef);
     Lit giveBoolVarDecisionPreferenceToSMTSolver(PTRef);
-    Lit giveAnyDecisionPreferenceToSMTSolver(PTRef, FrameId);
+    Lit giveAnyDecisionPreferenceToSMTSolver(PTRef, FrameId, PreprocessingContext const &);
 
     virtual sstat solve_(vec<FrameId> const & enabledFrames);