Fixes for sygus inference on quantifier free problems (#3202)

diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 78e9e639ac201901604b32efbd7867ce74bd81a8..471d68ff8eac53432d0a6f52f3c49aa826c0f364 100644 (file)
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -256,10 +256,11 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions,
 
   // quantify the body
   Trace("sygus-infer") << "Make inner sygus conjecture..." << std::endl;
+  body = body.negate();
   if (!qvars.empty())
   {
     Node bvl = nm->mkNode(BOUND_VAR_LIST, qvars);
-    body = nm->mkNode(EXISTS, bvl, body.negate());
+    body = nm->mkNode(EXISTS, bvl, body);
   }
 
   // sygus attribute to mark the conjecture as a sygus conjecture

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index fcec12d3964958d731b4ac790ca00017b215f6f3..a6eed127b3df6a90a5321fe9f28bd68a8b2f4384 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -452,17 +452,22 @@ Node CegSingleInv::getSolution(unsigned sol_index,
                                bool rconsSygus)
 {
   Assert( d_sol!=NULL );
-  Assert(!d_inst.empty());
   const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
   Node varList = Node::fromExpr( dt.getSygusVarList() );
   Node prog = d_quant[0][sol_index];
   std::vector< Node > vars;
   Node s;
-  if( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ){
+  // If it is unconstrained: either the variable does not appear in the
+  // conjecture or the conjecture can be solved without a single instantiation.
+  if (d_prog_to_sol_index.find(prog) == d_prog_to_sol_index.end()
+      || d_inst.empty())
+  {
     Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl;
     s = d_qe->getTermEnumeration()->getEnumerateTerm(
         TypeNode::fromType(dt.getSygusType()), 0);
-  }else{
+  }
+  else
+  {
     Trace("csi-sol") << "Get solution for " << prog << ", with skolems : ";
     sol_index = d_prog_to_sol_index[prog];
     d_sol->d_varList.clear();

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 6fdbfd0bcdb24edd5a246cb9e06500f92f7e57e4..aabc2f1f3b255735a6505831a31a8853f385bdf2 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -1160,7 +1160,7 @@ void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map)
     }
     // store in map
     Node fvar = d_quant[0][i];
-    Assert(fvar.getType() == bsol.getType());
+    Assert(fvar.getType().isComparableTo(bsol.getType()));
     sol_map[fvar] = bsol;
   }
 }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8c2950c3edd9b5e2001788036c0ad8865564aa1e..5579885c35f59f82baca3daf83dcca9ef2dff4a9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1676,6 +1676,9 @@ set(regress_1_tests
   regress1/sygus/inv-unused.sy
   regress1/sygus/issue2914.sy
   regress1/sygus/issue2935.sy
+  regress1/sygus/issue3199.smt2
+  regress1/sygus/issue3200.smt2
+  regress1/sygus/issue3201.smt2
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy

diff --git a/test/regress/regress1/sygus/issue3199.smt2 b/test/regress/regress1/sygus/issue3199.smt2
new file mode 100644 (file)
index 0000000..b4681e3
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3199.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+; COMMAND-LINE: --sygus-inference
+(set-logic QF_LRA)
+(declare-fun v () Real)
+(assert (= v 0))
+(check-sat)
+(exit)

diff --git a/test/regress/regress1/sygus/issue3200.smt2 b/test/regress/regress1/sygus/issue3200.smt2
new file mode 100644 (file)
index 0000000..8eb144c
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3200.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+; COMMAND-LINE: --sygus-inference
+(set-logic ALL)
+(declare-fun v () Real)
+(assert (= (* v v) 0))
+(check-sat)
+(exit)

diff --git a/test/regress/regress1/sygus/issue3201.smt2 b/test/regress/regress1/sygus/issue3201.smt2
new file mode 100644 (file)
index 0000000..99a5550
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3201.smt2
@@ -0,0 +1,8 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-inference
+(set-logic ALL)
+(declare-fun v () Bool)
+(assert false)
+(assert v)
+(check-sat)
+(exit)