From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 20 Aug 2019 22:18:02 +0000 (-0500)
Subject: Fixes for sygus inference on quantifier free problems (#3202)
X-Git-Tag: cvc5-1.0.0~4003
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b967cc5c8d84023c1b821c59b7bca736ffda6bed;p=cvc5.git

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 78e9e639a..471d68ff8 100644
--- 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 fcec12d39..a6eed127b 100644
--- 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 6fdbfd0bc..aabc2f1f3 100644
--- 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 8c2950c3e..5579885c3 100644
--- 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
index 000000000..b4681e35e
--- /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
index 000000000..8eb144c61
--- /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
index 000000000..99a555010
--- /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)