Allow sygus in incremental mode (#7756)

This allows the basic use of SyGuS in incremental mode, where constraints can be pushed/popped.

It does not yet support getting multiple solutions for the same set of constraints, which will require more significant changes.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 5924ecde6c708026aa101a1cb8379431543305f4..8ecf3340f73f5b521d4e3f797d8d7e7461e423a6 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -371,7 +371,8 @@ command [std::unique_ptr<cvc5::Command>* cmd]
     }
   | /* check-sat */
     CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { if (PARSER_STATE->sygus()) {
+    {
+      if (PARSER_STATE->sygus()) {
         PARSER_STATE->parseError("Sygus does not support check-sat command.");
       }
       cmd->reset(new CheckSatCommand());
@@ -405,10 +406,6 @@ command [std::unique_ptr<cvc5::Command>* cmd]
     { cmd->reset(new GetDifficultyCommand); }
   | /* push */
     PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { if( PARSER_STATE->sygus() ){
-        PARSER_STATE->parseError("Sygus does not support push command.");
-      }
-    }
     ( k=INTEGER_LITERAL
       { unsigned num = AntlrInput::tokenToUnsigned(k);
         if(num == 0) {
@@ -438,10 +435,6 @@ command [std::unique_ptr<cvc5::Command>* cmd]
         }
       } )
   | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { if( PARSER_STATE->sygus() ){
-        PARSER_STATE->parseError("Sygus does not support pop command.");
-      }
-    }
     ( k=INTEGER_LITERAL
       { unsigned num = AntlrInput::tokenToUnsigned(k);
         // we don't compare num to PARSER_STATE->scopeLevel() here, since

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 2e4461c1cd75c6677fd72df0cf1aa4c54ae52b74..12a178814bfde8719c9d94a742d13e2549f7e47e 100644 (file)
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -185,12 +185,6 @@ void SygusSolver::assertSygusInvConstraint(Node inv,
 
 Result SygusSolver::checkSynth(Assertions& as)
 {
-  if (options().base.incrementalSolving)
-  {
-    // TODO (project #7)
-    throw ModalException(
-        "Cannot make check-synth commands when incremental solving is enabled");
-  }
   Trace("smt") << "SygusSolver::checkSynth" << std::endl;
   // if applicable, check if the subsolver is the correct one
   if (usingSygusSubsolver() && d_subsolverCd.get() != d_subsolver.get())
@@ -200,6 +194,11 @@ Result SygusSolver::checkSynth(Assertions& as)
     // the subsolver.
     d_sygusConjectureStale = true;
   }
+  // TODO (project #7): we currently must always rebuild the synthesis
+  // conjecture + subsolver, since it answers unsat. When the subsolver is
+  // updated to treat "sat" as solution for synthesis conjecture, this line
+  // will be deleted.
+  d_sygusConjectureStale = true;
   if (d_sygusConjectureStale)
   {
     NodeManager* nm = NodeManager::currentNM();

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8c79b292ab04ca4824a82e21e7606579040db310..cb4160f582c65be2b70a322efcd4d3a724e224a9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1306,6 +1306,7 @@ set(regress_0_tests
   regress0/sygus/General_plus10.sy
   regress0/sygus/hd-05-d1-prog-nogrammar.sy
   regress0/sygus/ho-occ-synth-fun.sy
+  regress0/sygus/incremental-modify-ex.sy
   regress0/sygus/inv-different-var-order.sy
   regress0/sygus/issue3356-syg-inf-usort.smt2
   regress0/sygus/issue3624.sy

diff --git a/test/regress/regress0/sygus/incremental-modify-ex.sy b/test/regress/regress0/sygus/incremental-modify-ex.sy
new file mode 100644 (file)
index 0000000..f453964
--- /dev/null
+++ b/test/regress/regress0/sygus/incremental-modify-ex.sy
@@ -0,0 +1,26 @@
+; COMMAND-LINE: -i --sygus-out=status
+;EXPECT: unsat
+;EXPECT: unsat
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Int
+  ((Start Int) (StartBool Bool))
+  ((Start Int (0 1 x y
+               (+ Start Start)
+               (- Start Start)
+               (ite StartBool Start Start)))
+   (StartBool Bool ((and StartBool StartBool)
+                    (not StartBool)
+                    (<= Start Start)))))
+
+
+(declare-var x Int)
+(declare-var y Int)
+
+(push 1)
+(constraint (>= (f x y) 0))
+(check-synth)
+(pop 1)
+
+(constraint (< (f x y) 0))
+(check-synth)