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

3 files changed, 11 insertions, 5 deletions

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;
   }
 }