Synth-check and accelerate options for sygus-rr (#1691)

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index c40491a40d688c14ee1638dd6769adbc25ffb496..ad05aa5cd2044c63281c5ebe442377acdb0fe416 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1147,6 +1147,21 @@ header = "options/quantifiers_options.h"
   read_only  = true
   help       = "when applicable, use grammar for choosing sample points"
 
+[[option]]
+  name       = "sygusRewSynthAccel"
+  category   = "regular"
+  long       = "sygus-rr-synth-accel"
+  type       = "bool"
+  default    = "false"
+  help       = "add dynamic symmetry breaking clauses based on candidate rewrites"
+
+[[option]]
+  name       = "sygusRewSynthCheck"
+  category   = "regular"
+  long       = "sygus-rr-synth-check"
+  type       = "bool"
+  default    = "false"
+  help       = "use satisfiability check to verify correctness of candidate rewrites"
 
 # CEGQI applied to general quantified formulas
 

diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index 2273db5ea44e39754bfbd536332be793e2205495..98855a7cac9004cdc32b8c705456a0d1789cbd7c 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -19,12 +19,14 @@
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
 #include "prop/prop_engine.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/skolemize.h"
+#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/theory_engine.h"
@@ -615,28 +617,98 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
           // e.g. one that is alpha-equivalent to another.
           if (!eq_sol.isNull())
           {
-            // The analog of terms sol and eq_sol are equivalent under sample
-            // points but do not rewrite to the same term. Hence, this indicates
-            // a candidate rewrite.
-            Printer* p = Printer::getPrinter(options::outputLanguage());
-            out << "(candidate-rewrite ";
-            p->toStreamSygus(out, sol);
-            out << " ";
-            p->toStreamSygus(out, eq_sol);
-            out << ")" << std::endl;
-            ++(cei->d_statistics.d_candidate_rewrites_print);
-            // debugging information
-            if (Trace.isOn("sygus-rr-debug"))
+            ExtendedRewriter* er = sygusDb->getExtRewriter();
+            Node solb = sygusDb->sygusToBuiltin(sol);
+            Node solbr = er->extendedRewrite(solb);
+            Node eq_solb = sygusDb->sygusToBuiltin(eq_sol);
+            Node eq_solr = er->extendedRewrite(eq_solb);
+            bool success = true;
+            bool verified = false;
+            // verify it if applicable
+            if (options::sygusRewSynthCheck())
+            {
+              Trace("rr-check") << "Check candidate rewrite..." << std::endl;
+              // Notice we don't set produce-models. rrChecker takes the same
+              // options as the SmtEngine we belong to, where we ensure that
+              // produce-models is set.
+              SmtEngine rrChecker(NodeManager::currentNM()->toExprManager());
+              rrChecker.setLogic(smt::currentSmtEngine()->getLogicInfo());
+              Node crr = solbr.eqNode(eq_solr).negate();
+              Trace("rr-check")
+                  << "Check candidate rewrite : " << crr << std::endl;
+              rrChecker.assertFormula(crr.toExpr());
+              Result r = rrChecker.checkSat();
+              Trace("rr-check") << "...result : " << r << std::endl;
+              if (r.asSatisfiabilityResult().isUnknown()
+                  || r.asSatisfiabilityResult().isSat())
+              {
+                Trace("rr-check")
+                    << "...rewrite does not hold for: " << std::endl;
+                success = false;
+                std::vector<Node> vars;
+                d_sampler[prog].getVariables(vars);
+                std::vector<Node> pt;
+                for (const Node& v : vars)
+                {
+                  Node val = Node::fromExpr(rrChecker.getValue(v.toExpr()));
+                  Trace("rr-check") << "  " << v << " -> " << val << std::endl;
+                  pt.push_back(val);
+                }
+                d_sampler[prog].addSamplePoint(pt);
+                // add the solution again
+                Node eq_sol_new = its->second.registerTerm(sol);
+                Assert(!r.asSatisfiabilityResult().isSat()
+                       || eq_sol_new == sol);
+              }
+              else
+              {
+                verified = true;
+              }
+            }
+            if (success)
             {
-              ExtendedRewriter* er = sygusDb->getExtRewriter();
-              Node solb = sygusDb->sygusToBuiltin(sol);
-              Node solbr = er->extendedRewrite(solb);
-              Node eq_solb = sygusDb->sygusToBuiltin(eq_sol);
-              Node eq_solr = er->extendedRewrite(eq_solb);
-              Trace("sygus-rr-debug")
-                  << "; candidate #1 ext-rewrites to: " << solbr << std::endl;
-              Trace("sygus-rr-debug")
-                  << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl;
+              // The analog of terms sol and eq_sol are equivalent under sample
+              // points but do not rewrite to the same term. Hence, this
+              // indicates a candidate rewrite.
+              Printer* p = Printer::getPrinter(options::outputLanguage());
+              out << "(" << (verified ? "" : "candidate-") << "rewrite ";
+              p->toStreamSygus(out, sol);
+              out << " ";
+              p->toStreamSygus(out, eq_sol);
+              out << ")" << std::endl;
+              ++(cei->d_statistics.d_candidate_rewrites_print);
+              // debugging information
+              if (Trace.isOn("sygus-rr-debug"))
+              {
+                Trace("sygus-rr-debug")
+                    << "; candidate #1 ext-rewrites to: " << solbr << std::endl;
+                Trace("sygus-rr-debug")
+                    << "; candidate #2 ext-rewrites to: " << eq_solr
+                    << std::endl;
+              }
+              if (options::sygusRewSynthAccel())
+              {
+                // Add a symmetry breaking clause that excludes the larger
+                // of sol and eq_sol. This effectively states that we no longer
+                // wish to enumerate any term that contains sol (resp. eq_sol)
+                // as a subterm.
+                Node exc_sol = sol;
+                unsigned sz = sygusDb->getSygusTermSize(sol);
+                unsigned eqsz = sygusDb->getSygusTermSize(eq_sol);
+                if (eqsz > sz)
+                {
+                  sz = eqsz;
+                  exc_sol = eq_sol;
+                }
+                TypeNode ptn = prog.getType();
+                Node x = sygusDb->getFreeVar(ptn, 0);
+                Node lem = sygusDb->getExplain()->getExplanationForEquality(
+                    x, exc_sol);
+                lem = lem.negate();
+                Trace("sygus-rr-sb")
+                    << "Symmetry breaking lemma : " << lem << std::endl;
+                sygusDb->registerSymBreakLemma(d_candidates[i], lem, ptn, sz);
+              }
             }
           }
         }