From b967cc5c8d84023c1b821c59b7bca736ffda6bed Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 20 Aug 2019 17:18:02 -0500 Subject: [PATCH] Fixes for sygus inference on quantifier free problems (#3202) --- src/preprocessing/passes/sygus_inference.cpp | 3 ++- src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 11 ++++++++--- src/theory/quantifiers/sygus/synth_conjecture.cpp | 2 +- test/regress/CMakeLists.txt | 3 +++ test/regress/regress1/sygus/issue3199.smt2 | 7 +++++++ test/regress/regress1/sygus/issue3200.smt2 | 7 +++++++ test/regress/regress1/sygus/issue3201.smt2 | 8 ++++++++ 7 files changed, 36 insertions(+), 5 deletions(-) create mode 100644 test/regress/regress1/sygus/issue3199.smt2 create mode 100644 test/regress/regress1/sygus/issue3200.smt2 create mode 100644 test/regress/regress1/sygus/issue3201.smt2 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& 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& 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) -- 2.30.2