From df7333de4436d846da70857e61cda411d22d02ba Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Mar 2020 14:04:32 -0500 Subject: [PATCH] Simplify auxiliary variable handling in CEGQI (#4141) Fixes #3849 and fixes #4062. Overall, the effect of this PR is that CEGQI will generate better instantiations more frequently for quantified formulas that involve the introduction of auxiliary variables. In CEGQI, auxiliary variables introduced in CEX lemmas must be given special treatment (since the instantiations should not involve them, thus they must be solved for as well). Previously, auxiliary variables that are introduced as parts of CEX lemmas were currently assumed to be: (1) Only occurring from ITE removal, e.g. s[(ite C t1 t2]) ---> s[k] ^ ite( C, k = t1, k = t2 ) (2) Always trivially solvable by looking at which literal was asserted (k = t1 or k = t2). Both of these assumption do not hold in general (aux variables can come from other kinds of terms e.g. choice functions, and the user can force options that rewrite arithmetic equalities to inequalities). This makes auxiliary variable handling in CEGQI more robust by treating auxiliary variables as standard variables. Effectively, this means that the entire procedure for determining instantiations is run for auxiliary variables. This PR removes the specific hacks that were used previously that were based on the assumptions above. Additionally, #3849 triggered a second issue: SyGuS solution reconstruction that involves auxiliary variables that are introduced as part of instantiation lemmas should not be considered valid solutions. Previously, only a warning was given. --- .../quantifiers/cegqi/ceg_instantiator.cpp | 114 +----------------- .../quantifiers/cegqi/ceg_instantiator.h | 38 +----- .../sygus/ce_guided_single_inv.cpp | 16 +-- test/regress/CMakeLists.txt | 1 + .../quantifiers/issue4062-cegqi-aux.smt2 | 9 ++ 5 files changed, 26 insertions(+), 152 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2 diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 0dc8f262e..f81b0e160 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -543,20 +543,11 @@ void CegInstantiator::registerTheoryId(TheoryId tid) } } -void CegInstantiator::registerVariable(Node v, bool is_aux) +void CegInstantiator::registerVariable(Node v) { Assert(std::find(d_vars.begin(), d_vars.end(), v) == d_vars.end()); - Assert(std::find(d_aux_vars.begin(), d_aux_vars.end(), v) - == d_aux_vars.end()); - if (!is_aux) - { - d_vars.push_back(v); - d_vars_set.insert(v); - } - else - { - d_aux_vars.push_back(v); - } + d_vars.push_back(v); + d_vars_set.insert(v); TypeNode vtn = v.getType(); Trace("cbqi-proc-debug") << "Collect theory ids from type " << vtn << " of " << v << std::endl; @@ -1410,15 +1401,14 @@ void CegInstantiator::presolve( Node q ) { } void CegInstantiator::processAssertions() { - Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() << ", #aux-var = " << d_aux_vars.size() << std::endl; + Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() + << std::endl; d_curr_asserts.clear(); d_curr_eqc.clear(); d_curr_type_eqc.clear(); // must use master equality engine to avoid value instantiations eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); - //to eliminate identified illegal terms - std::map< Node, Node > aux_subs; //for each variable for( unsigned i=0; i >::iterator itae = d_aux_eq.find( lit ); - if( itae!=d_aux_eq.end() ){ - for( std::map< Node, Node >::iterator itae2 = itae->second.begin(); itae2 != itae->second.end(); ++itae2 ){ - aux_subs[ itae2->first ] = itae2->second; - Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl; - } - } - }else if( atom.getKind()==BOOLEAN_TERM_VARIABLE ){ - if( std::find( d_aux_vars.begin(), d_aux_vars.end(), atom )!=d_aux_vars.end() ){ - Node val = NodeManager::currentNM()->mkConst( lit.getKind()!=NOT ); - aux_subs[ atom ] = val; - Trace("cbqi-proc") << "......add substitution : " << atom << " -> " << val << std::endl; - } - } } } } @@ -1501,43 +1476,6 @@ void CegInstantiator::processAssertions() { } ++eqcs_i; } - //construct substitution from auxiliary variable equalities (if e.g. ITE removal was applied to CE body of quantified formula) - std::vector< Node > subs_lhs; - std::vector< Node > subs_rhs; - for( unsigned i=0; i::iterator it = aux_subs.find( r ); - if( it!=aux_subs.end() ){ - addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second ); - }else{ - Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!! type is " << r.getType() << std::endl; - Assert(false); - } - } - - //apply substitutions to everything, if necessary - if( !subs_lhs.empty() ){ - Trace("cbqi-proc") << "Applying substitution : " << std::endl; - for( unsigned i=0; i " << subs_rhs[i] << std::endl; - } - for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){ - for( unsigned i=0; isecond.size(); i++ ){ - Node lit = it->second[i]; - lit = lit.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); - lit = Rewriter::rewrite( lit ); - it->second[i] = lit; - } - } - for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){ - for( unsigned i=0; isecond.size(); i++ ){ - Node n = it->second[i]; - n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); - n = Rewriter::rewrite( n ); - it->second[i] = n; - } - } - } //remove unecessary assertions for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){ @@ -1574,23 +1512,6 @@ void CegInstantiator::processAssertions() { } } -void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ) { - r = r.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); - - std::vector< Node > cl; - cl.push_back( l ); - std::vector< Node > cr; - cr.push_back( r ); - for( unsigned i=0; igetModel()->getValue( n ); } @@ -1687,12 +1608,9 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st //remove ITEs IteSkolemMap iteSkolemMap; d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap); - //Assert( d_aux_vars.empty() ); - d_aux_vars.clear(); - d_aux_eq.clear(); for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { Trace("cbqi-reg") << " register aux variable : " << i->first << std::endl; - registerVariable(i->first, true); + registerVariable(i->first); } for( unsigned i=0; i& lems, st // collect below are identical to the atoms that we add to the CNF stream rlem = d_qe->getTheoryEngine()->preprocess(rlem); Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl; - //record the literals that imply auxiliary variables to be equal to terms - if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){ - if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){ - if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][1][0] )!=d_aux_vars.end() ){ - Node v = lems[i][1][0]; - for( unsigned r=1; r<=2; r++ ){ - d_aux_eq[rlem[r]][v] = lems[i][r][1]; - Trace("cbqi-debug") << " " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl; - } - } - } - } - /*else if( lems[i].getKind()==EQUAL && lems[i][0].getType().isBoolean() ){ - //Boolean terms - if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][0] )!=d_aux_vars.end() ){ - Node v = lems[i][0]; - d_aux_eq[rlem][v] = lems[i][1]; - Trace("cbqi-debug") << " " << rlem << " implies " << v << " = " << lems[i][1] << std::endl; - } - }*/ lems[i] = rlem; } // determine variable order: must do Reals before Ints diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 76e0869fa..b4aa38c07 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -396,15 +396,6 @@ class CegInstantiator { * such as the above data structures. */ void processAssertions(); - /** add to auxiliary variable substitution - * This adds the substitution l -> r to the auxiliary - * variable substitution subs_lhs -> subs_rhs, and serializes - * it (applies it to existing substitutions). - */ - void addToAuxVarSubstitution(std::vector& subs_lhs, - std::vector& subs_rhs, - Node l, - Node r); /** cache bound variables for type returned * by getBoundVariable(...). */ @@ -462,35 +453,8 @@ class CegInstantiator { * and sending on the output channel of this class. */ std::vector d_input_vars; - /** literals to equalities for aux vars - * This stores entries of the form - * L -> ( k -> t ) - * where - * k is a variable in d_aux_vars, - * L is a literal that if asserted implies that our - * instantiation should map { k -> t }. - * For example, if a term of the form - * ite( C, t1, t2 ) - * was replaced by k, we get this (top-level) assertion: - * ite( C, k=t1, k=t2 ) - * The vector d_aux_eq contains the exact form of - * the literals in the above constraint that they would - * appear in assertions, meaning d_aux_eq may contain: - * t1=k -> ( k -> t1 ) - * t2=k -> ( k -> t2 ) - * where t1=k and t2=k are the rewritten form of - * k=t1 and k=t2 respectively. - */ - std::map > d_aux_eq; - /** auxiliary variables - * These variables include the result of removing ITE - * terms from the quantified formula we are processing. - * These variables must be eliminated from constraints - * as a preprocess step to check(). - */ - std::vector d_aux_vars; /** register variable */ - void registerVariable(Node v, bool is_aux = false); + void registerVariable(Node v); //-------------------------------the variables //-------------------------------quantified formula info diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 2e5a834b1..27d77dfbb 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -564,13 +564,15 @@ Node CegSingleInv::reconstructToSyntax(Node s, } } - - if( Trace.isOn("csi-sol") ){ - //debug solution - if (!d_sol->debugSolution(d_solution)) - { - Trace("csi-sol") << "WARNING : solution " << d_solution << " contains free constants." << std::endl; - } + // debug solution + if (!d_sol->debugSolution(d_solution)) + { + // This can happen if we encountered free variables in either the + // instantiation terms, or in the instantiation lemmas after postprocessing. + // In this case, we fail, since the solution is not valid. + Trace("csi-sol") << "FAIL : solution " << d_solution + << " contains free constants." << std::endl; + reconstructed = -1; } if( Trace.isOn("cegqi-stats") ){ int tsize, itesize; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cd83ef3d1..4cd3c70d2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1502,6 +1502,7 @@ set(regress_1_tests regress1/quantifiers/issue3765.smt2 regress1/quantifiers/issue3765-quant-dd.smt2 regress1/quantifiers/issue4021-ind-opts.smt2 + regress1/quantifiers/issue4062-cegqi-aux.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lra-vts-inf.smt2 diff --git a/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2 b/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2 new file mode 100644 index 000000000..0296c978c --- /dev/null +++ b/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --arith-rewrite-equalities --global-negate --no-check-models +; EXPECT: sat +(set-logic NIA) +(set-option :arith-rewrite-equalities true) +(set-option :global-negate true) +(set-info :status sat) +(declare-const i5 Int) +(assert (= 562 (abs i5))) +(check-sat) -- 2.30.2