From: Andrew Reynolds Date: Wed, 21 Nov 2018 22:24:16 +0000 (-0600) Subject: Quickly recognize when PBE conjectures are infeasible (#2718) X-Git-Tag: cvc5-1.0.0~4358 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1e7ce9dcc5268c8e13466f63ac2c4159d71a583a;p=cvc5.git Quickly recognize when PBE conjectures are infeasible (#2718) Recognizes when the conjecture has conflicting I/O pairs. Also includes a minor change to the default behavior of PBE. This change broke a delicate regression array_search_2, which I fixed by adding some additional options to make it more robust. After this PR, we immediately find 4/7 unsolved in PBE strings of sygusComp 2018 to be infeasible. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f3a6c0c9e..7bf86f092 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1304,6 +1304,14 @@ void SmtEngine::setDefaults() { options::unconstrainedSimp.set(uncSimp); } } + if (!options::proof()) + { + // minimizing solutions from single invocation requires proofs + if (options::cegqiSolMinCore() && options::cegqiSolMinCore.wasSetByUser()) + { + throw OptionException("cegqi-si-sol-min-core requires --proof"); + } + } // Disable options incompatible with unsat cores and proofs or output an // error if enabled explicitly diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index ee7247121..408f076ac 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -16,9 +16,10 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" +#include "theory/datatypes/datatypes_rewriter.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "util/random.h" using namespace CVC4; @@ -40,7 +41,7 @@ SygusPbe::~SygusPbe() {} //--------------------------------- collecting finite input/output domain information -void SygusPbe::collectExamples(Node n, +bool SygusPbe::collectExamples(Node n, std::map& visited, bool hasPol, bool pol) @@ -54,10 +55,12 @@ void SygusPbe::collectExamples(Node n, { neval = n; if( hasPol ){ - n_output = !pol ? d_true : d_false; + n_output = pol ? d_true : d_false; } neval_is_evalapp = true; - }else if( n.getKind()==EQUAL && hasPol && !pol ){ + } + else if (n.getKind() == EQUAL && hasPol && pol) + { for( unsigned r=0; r<2; r++ ){ if (n[r].getKind() == DT_SYGUS_EVAL) { @@ -72,6 +75,25 @@ void SygusPbe::collectExamples(Node n, // is it an evaluation function? if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end()) { + Trace("sygus-pbe-debug") + << "Process head: " << n << " == " << n_output << std::endl; + // If n_output is null, then neval does not have a constant value + // If n_output is non-null, then neval is constrained to always be + // that value. + if (!n_output.isNull()) + { + std::map::iterator itet = d_exampleTermMap.find(neval); + if (itet == d_exampleTermMap.end()) + { + d_exampleTermMap[neval] = n_output; + } + else if (itet->second != n_output) + { + // We have a conflicting pair f( c ) = d1 ^ f( c ) = d2 for d1 != d2, + // the conjecture is infeasible. + return false; + } + } // get the evaluation head Node eh = neval[0]; std::map::iterator itx = d_examples_invalid.find(eh); @@ -103,7 +125,7 @@ void SygusPbe::collectExamples(Node n, Assert(n_output.isConst()); } // finished processing this node - return; + return true; } d_examples_invalid[eh] = true; d_examples_out_invalid[eh] = true; @@ -112,10 +134,14 @@ void SygusPbe::collectExamples(Node n, for( unsigned i=0; i& lemmas) { Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl; + NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0; i < candidates.size(); i++) { @@ -133,7 +160,14 @@ bool SygusPbe::initialize(Node n, } std::map visited; - collectExamples(n, visited, true, true); + // n is negated conjecture + if (!collectExamples(n, visited, true, false)) + { + Trace("sygus-pbe") << "...conflicting examples" << std::endl; + Node infeasible = d_parent->getGuard().negate(); + lemmas.push_back(infeasible); + return false; + } for (unsigned i = 0; i < candidates.size(); i++) { @@ -198,7 +232,6 @@ bool SygusPbe::initialize(Node n, tn_to_strategy_pt[tnsp].push_back(p.first); } // initialize the enumerators - NodeManager* nm = NodeManager::currentNM(); for (const Node& e : d_candidate_to_enum[c]) { TypeNode etn = e.getType(); diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index e21c9263f..a62100692 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -240,11 +240,17 @@ class SygusPbe : public SygusModule * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 ) */ std::map > d_examples_term; + /** + * Map from example input terms to their output, for example [EX#1] above, + * this is { f( 0 ) -> 2, f( 5 ) -> 7, f( 6 ) -> 8 }. + */ + std::map d_exampleTermMap; /** collect the PBE examples in n - * This is called on the input conjecture, and will populate the above vectors. - * hasPol/pol denote the polarity of n in the conjecture. - */ - void collectExamples(Node n, + * This is called on the input conjecture, and will populate the above + * vectors, where hasPol/pol denote the polarity of n in the conjecture. This + * function returns false if it finds two examples that are contradictory. + */ + bool collectExamples(Node n, std::map& visited, bool hasPol, bool pol); diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 78892aac8..4bd6cb7fe 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -701,12 +701,12 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) Trace("sygus-sui-enum") << " ...fail : term is not unique" << std::endl; } - d_cond_count++; } if (keep) { // notify to retry the build of solution d_check_sol = true; + d_cond_count++; ecv.addEnumValue(v, results); } } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 2bfde2d80..e1cbed044 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -78,6 +78,12 @@ void SynthConjecture::assign(Node q) d_quant = q; NodeManager* nm = NodeManager::currentNM(); + // initialize the guard + d_feasible_guard = nm->mkSkolem("G", nm->booleanType()); + d_feasible_guard = Rewriter::rewrite(d_feasible_guard); + d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard); + AlwaysAssert(!d_feasible_guard.isNull()); + // pre-simplify the quantified formula based on the process utility d_simp_quant = d_ceg_proc->preSimplify(d_quant); @@ -177,11 +183,6 @@ void SynthConjecture::assign(Node q) } } - // initialize the guard - d_feasible_guard = nm->mkSkolem("G", nm->booleanType()); - d_feasible_guard = Rewriter::rewrite(d_feasible_guard); - d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard); - AlwaysAssert(!d_feasible_guard.isNull()); // register the strategy d_feasible_strategy.reset( new DecisionStrategySingleton("sygus_feasible", diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a1d5a35aa..97b1fb99b 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -861,6 +861,7 @@ set(regress_0_tests regress0/sygus/real-si-all.sy regress0/sygus/strings-unconstrained.sy regress0/sygus/uminus_one.sy + regress0/sygus/univ_3-long-repeat-conflict.sy regress0/test11.cvc regress0/test9.cvc regress0/tptp/ARI086=1.p diff --git a/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy new file mode 100644 index 000000000..c2ed642be --- /dev/null +++ b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy @@ -0,0 +1,50 @@ +; EXPECT: unknown +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) + +(synth-fun f ((col1 String) (col2 String)) String + ((Start String (ntString)) + (ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY" + (str.++ ntString ntString) + (str.replace ntString ntString ntString) + (str.at ntString ntInt) + (int.to.str ntInt) + (ite ntBool ntString ntString) + (str.substr ntString ntInt ntInt))) + (ntInt Int (0 1 2 + (+ ntInt ntInt) + (- ntInt ntInt) + (str.len ntString) + (str.to.int ntString) + (str.indexof ntString ntString ntInt))) + (ntBool Bool (true false + (str.prefixof ntString ntString) + (str.suffixof ntString ntString) + (str.contains ntString ntString))))) + + +(declare-var col1 String) +(declare-var col2 String) +(constraint (= (f "UC Berkeley" "Berkeley, CA") + "Berkeley, CA, USA")) +(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") + "Phialdelphia, PA, USA")) +(constraint (= (f "UCLA" "Los Angeles, CA") + "UCLA, Los Angeles, CA, USA")) +(constraint (= (f "Cornell University" "Ithaca, New York, USA") + "Ithaca, New York, USA")) +(constraint (= (f "Penn" "Philadelphia, PA, USA") + "Philadelphia, PA, USA")) +(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA") + "Ann Arbor, MI, USA")) +(constraint (= (f "UC Berkeley" "Berkeley, CA") + "Berkeley, CA, USA")) +(constraint (= (f "MIT" "Cambridge, MA") + "Cambridge, MA, USA")) +(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") + "Phialdelphia, PA, USA")) +(constraint (= (f "UCLA" "Los Angeles, CA") + "Los Angeles, CA, USA")) + +; has contradictory examples +(check-synth) diff --git a/test/regress/regress1/sygus/array_search_2.sy b/test/regress/regress1/sygus/array_search_2.sy index 41346e655..93cbf9ce9 100644 --- a/test/regress/regress1/sygus/array_search_2.sy +++ b/test/regress/regress1/sygus/array_search_2.sy @@ -1,5 +1,6 @@ +; REQUIRES: proof ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --cegqi-si-sol-min-core --proof (set-logic LIA) (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int)