Properly restrict PBE symmetry breaking for abduction queries (#7269)

This ensures we infer when a conjecture is PBE based on the conjecture plus the side condition for abduction. This fixes issues where the sygus solver was over-pruning solutions for abduction queries.

It also changes the names of internal symbols used for abduction/interpolation queries. These names are used when the experimental sygus-stream is used. These symbols are changed (from "A") to avoid confusion with user symbols.

diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index b66daefd36cae97c5723ae3811a6992904baa5cf..3bdf13efb7f1832b5553673efe628f984002fc7b 100644 (file)
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -53,7 +53,7 @@ bool AbductionSolver::getAbduct(const std::vector<Node>& axioms,
   conjn = conjn.negate();
   d_abdConj = conjn;
   asserts.push_back(conjn);
-  std::string name("A");
+  std::string name("__internal_abduct");
   Node aconj = quantifiers::SygusAbduct::mkAbductionConjecture(
       name, asserts, axioms, grammarType);
   // should be a quantified conjecture with one function-to-synthesize

diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index 3e227fa31f8552efec31e4fce41263e7a13482e1..ff8e14e9b1134a22490a00e2bdf59247b458ae22 100644 (file)
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -51,7 +51,7 @@ bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
                           << std::endl;
   // must expand definitions
   Node conjn = d_env.getTopLevelSubstitutions().apply(conj);
-  std::string name("A");
+  std::string name("__internal_interpol");
 
   quantifiers::SygusInterpol interpolSolver(d_env);
   if (interpolSolver.solveInterpolation(

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
index 1b5b3f5afffd082d954e58b65d3111a2cac92f23..1170eee82f9b0819424474dc301df3604de1e320 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
@@ -46,7 +46,7 @@ bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms)
   // First, must be unique up to rewriting
   if (bterms.find(bnr) != bterms.end())
   {
-    Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl;
+    Trace("sygus-enum-exc") << "Exclude (by rewriting): " << bn << std::endl;
     return false;
   }
   // insert to builtin term cache, regardless of whether it is redundant
@@ -55,8 +55,6 @@ bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms)
   // callback-specific add term
   if (!addTermInternal(n, bn, bnr))
   {
-    Trace("sygus-enum-exc")
-        << "Exclude: " << bn << " due to callback" << std::endl;
     return false;
   }
   Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index ab2a73cb0adf8bcdd22a26d8ecd9e5aaf7a36de4..4fa8ba78e50b29585138064d038c61f88ed5b325 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -204,7 +204,16 @@ void SynthConjecture::assign(Node q)
     }
   }
   // initialize the example inference utility
-  if (!d_exampleInfer->initialize(d_base_inst, d_candidates))
+  // Notice that we must also consider the side condition when inferring
+  // whether the conjecture is PBE. This ensures we do not prune solutions
+  // that may satisfy the side condition based on equivalence-up-to-examples
+  // with solutions that do not.
+  Node conjForExamples = d_base_inst;
+  if (!d_embedSideCondition.isNull())
+  {
+    conjForExamples = nm->mkNode(AND, d_embedSideCondition, d_base_inst);
+  }
+  if (d_exampleInfer!=nullptr && !d_exampleInfer->initialize(conjForExamples, d_candidates))
   {
     // there is a contradictory example pair, the conjecture is infeasible.
     Node infLem = d_feasible_guard.negate();
@@ -761,7 +770,7 @@ EnumValueManager* SynthConjecture::getEnumValueManagerFor(Node e)
   }
   // otherwise, allocate it
   Node f = d_tds->getSynthFunForEnumerator(e);
-  bool hasExamples = (d_exampleInfer->hasExamples(f)
+  bool hasExamples = (d_exampleInfer != nullptr && d_exampleInfer->hasExamples(f)
                       && d_exampleInfer->getNumExamples(f) != 0);
   d_enumManager[e].reset(new EnumValueManager(
       d_env, d_qstate, d_qim, d_treg, d_stats, e, hasExamples));

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 55b932f818176a9f02b35ffebd3a6646623c3554..3bfe356fac63121e58d5fd1bececd35c0eabccfd 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2283,6 +2283,7 @@ set(regress_1_tests
   regress1/sygus/abd-simple-conj-4.smt2
   regress1/sygus/abduction_1255.corecstrs.readable.smt2
   regress1/sygus/abduction_streq.readable.smt2
+  regress1/sygus/abduction-no-pbe-sym-break.smt2
   regress1/sygus/abv.sy
   regress1/sygus/array-grammar-store.sy
   regress1/sygus/array_search_5-Q-easy.sy

diff --git a/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2 b/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2
new file mode 100644 (file)
index 0000000..79fa4f2
--- /dev/null
+++ b/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+(set-logic UF)
+(set-option :produce-abducts true)
+(declare-const A Bool)
+(declare-const B Bool)
+(declare-const C Bool)
+(assert (=> A C))
+(get-abduct D (=> A B))