From 0ddf1b9c74f2b2a78e0960b710c2edbdc5f8d02d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 27 Aug 2015 17:27:57 +0200 Subject: [PATCH] Do ITE term bookkeeping when solving Sygus inputs. Add missing script from Sygus comp 2015. Fix bug 665 regarding strings rewriter for contains. --- contrib/run-script-syguscomp2015 | 17 +++++++ .../quantifiers/ce_guided_instantiation.cpp | 17 +++---- .../quantifiers/ce_guided_single_inv.cpp | 13 ++--- src/theory/quantifiers/ce_guided_single_inv.h | 4 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 38 +++++++++++++-- src/theory/quantifiers/inst_strategy_cbqi.h | 24 +++++----- .../quantifiers/instantiation_engine.cpp | 48 ++++++------------- .../strings/theory_strings_rewriter.cpp | 5 +- 8 files changed, 94 insertions(+), 72 deletions(-) create mode 100644 contrib/run-script-syguscomp2015 diff --git a/contrib/run-script-syguscomp2015 b/contrib/run-script-syguscomp2015 new file mode 100644 index 000000000..aab6851e1 --- /dev/null +++ b/contrib/run-script-syguscomp2015 @@ -0,0 +1,17 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function trywith { + ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench) 2>/dev/null | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} + +trywith --cegqi --cegqi-si-multi-inst-abort --cegqi-si-abort --decision=internal +trywith --cegqi --no-cegqi-si + diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index dce9c088c..f01efb5c4 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -87,16 +87,17 @@ void CegConjecture::initializeGuard( QuantifiersEngine * qe ){ if( !d_syntax_guided ){ //add immediate lemma Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), d_base_inst.negate() ); - Trace("cegqi") << "Add candidate lemma : " << lem << std::endl; + Trace("cegqi-lemma") << "Add candidate lemma : " << lem << std::endl; qe->getOutputChannel().lemma( lem ); }else if( d_ceg_si ){ - Node lem = d_ceg_si->getSingleInvLemma( d_guard ); - if( !lem.isNull() ){ - Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl; - qe->getOutputChannel().lemma( lem ); + std::vector< Node > lems; + d_ceg_si->getSingleInvLemma( d_guard, lems ); + for( unsigned i=0; igetOutputChannel().lemma( lems[i] ); if( Trace.isOn("cegqi-debug") ){ - lem = Rewriter::rewrite( lem ); - Trace("cegqi-debug") << "...rewritten : " << lem << std::endl; + Node rlem = Rewriter::rewrite( lems[i] ); + Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl; } } } @@ -279,7 +280,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if( !lems.empty() ){ d_last_inst_si = true; for( unsigned j=0; jaddLemma( lems[j] ); } d_statistics.d_cegqi_si_lemmas += lems.size(); diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index f122c63bb..c31ebd9ab 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -59,7 +59,7 @@ CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConje d_sol = new CegConjectureSingleInvSol( qe ); } -Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { +void CegConjectureSingleInv::getSingleInvLemma( Node guard, std::vector< Node >& lems ) { if( !d_single_inv.isNull() ) { d_single_inv_var.clear(); d_single_inv_sk.clear(); @@ -80,13 +80,10 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { inst = TermDb::simpleNegate( inst ); Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl; - //copy variables to instantiator - d_cinst->d_vars.clear(); - d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); - - return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst ); - }else{ - return Node::null(); + //register with the instantiator + Node ginst = NodeManager::currentNM()->mkNode( OR, guard.negate(), inst ); + lems.push_back( ginst ); + d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk ); } } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 7df859337..8950b2642 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -113,8 +113,8 @@ public: std::map< Node, Node > d_trans_post; std::map< Node, std::vector< Node > > d_prog_templ_vars; public: - //get the single invocation lemma - Node getSingleInvLemma( Node guard ); + //get the single invocation lemma(s) + void getSingleInvLemma( Node guard, std::vector< Node >& lems ); //initialize void initialize( Node q ); //check diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 41c0e276b..073cba525 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -9,7 +9,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Implementation of cbqi instantiation strategies + ** \brief Implementation of counterexample-guided quantifier instantiation strategies **/ #include "theory/quantifiers/inst_strategy_cbqi.h" @@ -20,6 +20,7 @@ #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/first_order_model.h" +#include "util/ite_removal.h" using namespace std; using namespace CVC4; @@ -28,7 +29,6 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::arith; -using namespace CVC4::theory::datatypes; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA //#define MBP_STRICT_ASSERTIONS @@ -1182,6 +1182,37 @@ void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, st subs_rhs.push_back( r ); } +void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) { + Assert( d_vars.empty() ); + d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() ); + IteSkolemMap iteSkolemMap; + d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap); + Assert( d_aux_vars.empty() ); + for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { + Trace("cbqi-debug") << " Auxiliary var (from ITE) : " << i->first << std::endl; + d_aux_vars.push_back( i->first ); + } + for( unsigned i=0; i > d_curr_eqc; std::map< Node, Node > d_curr_rep; std::vector< Node > d_curr_arith_eqc; + //auxiliary variables + std::vector< Node > d_aux_vars; + //literals to equalities for aux vars + std::map< Node, std::map< Node, Node > > d_aux_eq; + //the CE variables + std::vector< Node > d_vars; private: //for adding instantiations during check void computeProgVars( Node n ); @@ -87,16 +89,12 @@ private: void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); public: CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); - //the CE variables - std::vector< Node > d_vars; - //auxiliary variables - std::vector< Node > d_aux_vars; - //literals to equalities for aux vars - std::map< Node, std::map< Node, Node > > d_aux_eq; //check : add instantiations based on valuation of d_vars bool check(); //presolve for quantified formula void presolve( Node q ); + //register the counterexample lemma (stored in lems), modify vector + void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ); }; class InstStrategySimplex : public InstStrategy{ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 492b2dedf..699208fba 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -21,7 +21,6 @@ #include "theory/quantifiers/inst_strategy_e_matching.h" #include "theory/quantifiers/inst_strategy_cbqi.h" #include "theory/quantifiers/trigger.h" -#include "util/ite_removal.h" using namespace std; using namespace CVC4; @@ -108,44 +107,25 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ lem = Rewriter::rewrite( lem ); Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; - //must explicitly remove ITEs so that we record dependencies - IteSkolemMap iteSkolemMap; - std::vector< Node > lems; - lems.push_back( lem ); - d_quantEngine->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap); - CegInstantiator * cinst = NULL; if( d_i_cegqi ){ - cinst = d_i_cegqi->getInstantiator( f ); - Assert( cinst->d_aux_vars.empty() ); - for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { - Trace("cbqi-debug") << " Auxiliary var (from ITE) : " << i->first << std::endl; - cinst->d_aux_vars.push_back( i->first ); + //must register with the instantiator + //must explicitly remove ITEs so that we record dependencies + std::vector< Node > ce_vars; + for( int i=0; igetTermDatabase()->getNumInstantiationConstants( f ); i++ ){ + ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) ); } - } - for( unsigned i=0; i lems; + lems.push_back( lem ); + CegInstantiator * cinst = d_i_cegqi->getInstantiator( f ); + cinst->registerCounterexampleLemma( lems, ce_vars ); + for( unsigned i=0; iaddLemma( lems[i], false ); - }else{ - Node rlem = lems[i]; - rlem = Rewriter::rewrite( rlem ); - Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl; - d_quantEngine->addLemma( rlem, false ); - //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( cinst->d_aux_vars.begin(), cinst->d_aux_vars.end(), lems[i][1][0] )!=cinst->d_aux_vars.end() ){ - Node v = lems[i][1][0]; - for( unsigned r=1; r<=2; r++ ){ - cinst->d_aux_eq[rlem[r]][v] = lems[i][r][1]; - Trace("cbqi-debug") << " " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl; - } - } - } - } } + }else{ + Trace("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; + d_quantEngine->addLemma( lem, false ); } - addedLemma = true; } } diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 7023f7c41..872933cbd 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -948,8 +948,9 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { bool flag = false; unsigned n1 = node[0].getNumChildren(); unsigned n2 = node[1].getNumChildren(); - if(n1 - n2) { - for(unsigned i=0; i<=n1 - n2; i++) { + if( n1>n2 ){ + unsigned diff = n1-n2; + for(unsigned i=0; i