diff options
29 files changed, 607 insertions, 269 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5dfada655..4136c3163 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1442,7 +1442,8 @@ void SmtEngine::setDefaults() { }else{ //counterexample-guided instantiation for non-sygus // enable if any quantifiers with arithmetic or datatypes - if( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ){ + if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) || + options::cbqiAll() ){ if( !options::cbqi.wasSetByUser() ){ options::cbqi.set( true ); } @@ -1458,6 +1459,7 @@ void SmtEngine::setDefaults() { } } if( options::cbqi() && d_logic.isPure(THEORY_ARITH) ){ + options::cbqiAll.set( false ); if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); } diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 6ff72c1a2..26689c81a 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -167,10 +167,10 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ void DatatypesEnumerator::init(){ //Assert(type.isDatatype()); - Debug("te") << "datatype is datatype? " << d_type.isDatatype() << std::endl; - Debug("te") << "datatype is kind " << d_type.getKind() << std::endl; - Debug("te") << "datatype is " << d_type << std::endl; - Debug("te") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton() << " " << d_datatype.isFinite() << std::endl; + Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() << std::endl; + Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl; + Debug("dt-enum") << "datatype is " << d_type << std::endl; + Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton() << " " << d_datatype.isFinite() << std::endl; if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){ //start with uninterpreted constant @@ -181,12 +181,15 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ d_sel_sum.push_back( -1 ); }else{ // find the "zero" constructor via mkGroundTerm + Debug("dt-enum-debug") << "make ground term..." << std::endl; Node t = d_type.mkGroundTerm(); + Debug("dt-enum-debug") << "done : " << t << std::endl; Assert( t.getKind()==kind::APPLY_CONSTRUCTOR ); // start with the constructor for which a ground term is constructed d_zeroCtor = Datatype::indexOf( t.getOperator().toExpr() ); d_has_debruijn = 0; } + Debug("dt-enum") << "zero ctor : " << d_zeroCtor << std::endl; d_ctor = d_zeroCtor; for( unsigned i=0; i<d_datatype.getNumConstructors(); ++i ){ d_sel_types.push_back( std::vector< TypeNode >() ); diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 0e7b02b53..b67c4bd56 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -154,24 +154,31 @@ Node CandidateGeneratorQELitEq::getNextCandidate(){ CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) : d_match_pattern( mpat ), d_qe( qe ){ + Assert( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ); + d_match_pattern_type = d_match_pattern[0].getType(); } + void CandidateGeneratorQELitDeq::resetInstantiationRound(){ } + void CandidateGeneratorQELitDeq::reset( Node eqc ){ Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) ); d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() ); } + Node CandidateGeneratorQELitDeq::getNextCandidate(){ //get next candidate term in equivalence class while( !d_eqc_false.isFinished() ){ Node n = (*d_eqc_false); ++d_eqc_false; if( n.getKind()==d_match_pattern.getKind() ){ - //found an iff or equality, try to match it - //DO_THIS: cache to avoid redundancies? - //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false? - return n; + if( n[0].getType().isComparableTo( d_match_pattern_type ) ){ + //found an iff or equality, try to match it + //DO_THIS: cache to avoid redundancies? + //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false? + return n; + } } } return Node::null(); diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index 9d4035970..fb120dd08 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -126,6 +126,8 @@ private: eq::EqClassIterator d_eqc_false; //equality you are trying to match disequalities for Node d_match_pattern; + //type of disequality + TypeNode d_match_pattern_type; //einstantiator pointer QuantifiersEngine* d_qe; public: diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 3e69a616a..2530402ff 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -202,6 +202,21 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve } Node eq = eq_lhs.eqNode( eq_rhs ); eq = Rewriter::rewrite( eq ); + Node vts_coeff_inf; + Node vts_coeff_delta; + Node val; + Node veq_c; + //isolate pv in the equality + int ires = isolate( pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta ); + if( ires!=0 ){ + if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ + subs_proc[val][veq_c] = true; + if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + return true; + } + } + } + /* //cannot contain infinity? //if( !d_qe->getTermDatabase()->containsVtsInfinity( eq ) ){ Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; @@ -231,6 +246,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve } } } + */ } } lhs.push_back( ns ); @@ -787,14 +803,14 @@ bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node > } sf.d_subs[index] = veq[1]; if( !veq_c.isNull() ){ - sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c ); + sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c ); Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl; //intger division rounding up if from a lower bound if( btyp[index]==1 && options::cbqiRoundUpLowerLia() ){ sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index], NodeManager::currentNM()->mkNode( ITE, NodeManager::currentNM()->mkNode( EQUAL, - NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), + NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, veq[1], veq_c ), d_zero ), d_zero, d_one ) ); @@ -1423,7 +1439,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } //this isolates the monomial sum into solved form (pv k t), ensures t is Int if pv is Int, and t does not contain vts symbols -int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { +int CegInstantiator::isolate( Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { int ires = 0; Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl; std::map< Node, Node > msum; @@ -1468,6 +1484,12 @@ int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node if( ires!=0 ){ Node realPart; Trace("cbqi-inst-debug") << "Isolate : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; + if( options::cbqiAll() ){ + // when not pure LIA/LRA, we must check whether the lhs contains pv + if( TermDb::containsTerm( val, pv ) ){ + return 0; + } + } if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){ //redo, split integer/non-integer parts bool useCoeff = false; diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 47e838f1c..2b4854305 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -67,8 +67,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){ //make sure the matching portion of the equality is on the LHS of d_pattern // and record what d_match_pattern is - if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) || - d_match_pattern[0].getKind()==INST_CONSTANT ){ + if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) || d_match_pattern[0].getKind()==INST_CONSTANT ){ if( d_match_pattern[1].getKind()!=INST_CONSTANT ){ Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) ); Node mp = d_match_pattern[1]; @@ -83,8 +82,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern; d_match_pattern = mp; } - }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) || - d_match_pattern[1].getKind()==INST_CONSTANT ){ + }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) || d_match_pattern[1].getKind()==INST_CONSTANT ){ if( d_match_pattern[0].getKind()!=INST_CONSTANT ){ Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) ); if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching @@ -463,7 +461,7 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node q, InstMatch& m, QuantifiersE Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl; Node s = d_subs.substitute( d_var, d_eq_class ); s = Rewriter::rewrite( s ); - Trace("var-trigger-matching") << "...got " << s << std::endl; + Trace("var-trigger-matching") << "...got " << s << ", " << s.getKind() << std::endl; d_eq_class = Node::null(); //if( s.getType().isSubtypeOf( d_var_type ) ){ d_rm_prev = m.get( d_var_num[0] ).isNull(); diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 56d5022c4..39cde56e8 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -102,8 +102,13 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ + double clSet = 0; + if( Trace.isOn("cbqi-engine") ){ + clSet = double(clock())/double(CLOCKS_PER_SEC); + Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl; + } + unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); for( int ee=0; ee<=1; ee++ ){ - unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ @@ -114,6 +119,13 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { break; } } + if( Trace.isOn("cbqi-engine") ){ + if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ + Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; + } + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl; + } } } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 928c15593..09cf9d2eb 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -29,16 +29,11 @@ using namespace CVC4::theory::inst; using namespace CVC4::theory::quantifiers; //priority levels : -//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={ignore,resort}) +//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={resort,ignore}) //2 : user patterns (when user-pat=resort), auto gen patterns (for user pattern quantifiers when user-pat=use) -//3 : -//4 : -//5 : full saturate quantifiers // user-pat=interleave alternates between use and resort -//#define MULTI_TRIGGER_FULL_EFFORT_HALF - struct sortQuantifiersForSymbol { QuantifiersEngine* d_qe; bool operator() (Node i, Node j) { @@ -57,7 +52,7 @@ struct sortQuantifiersForSymbol { void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){ //reset triggers for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){ - for( int i=0; i<(int)it->second.size(); i++ ){ + for( unsigned i=0; i<it->second.size(); i++ ){ it->second[i]->resetInstantiationRound(); it->second[i]->reset( Node::null() ); } @@ -107,27 +102,27 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ return STATUS_UNKNOWN; } -void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ +void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){ Assert( pat.getKind()==INST_PATTERN ); //add to generators bool usable = true; std::vector< Node > nodes; - for( int i=0; i<(int)pat.getNumChildren(); i++ ){ + for( unsigned i=0; i<pat.getNumChildren(); i++ ){ nodes.push_back( pat[i] ); - if( pat[i].getKind()!=INST_CONSTANT && !Trigger::isUsableTrigger( pat[i], f ) ){ + if( pat[i].getKind()!=INST_CONSTANT && !Trigger::isUsableTrigger( pat[i], q ) ){ Trace("trigger-warn") << "User-provided trigger is not usable : " << pat << " because of " << pat[i] << std::endl; usable = false; break; } } if( usable ){ - Trace("user-pat") << "Add user pattern: " << pat << " for " << f << std::endl; + Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl; //check match option int matchOption = 0; if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){ - d_user_gen_wait[f].push_back( nodes ); + d_user_gen_wait[q].push_back( nodes ); }else{ - d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) ); + d_user_gen[q].push_back( Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) ); } } } @@ -386,18 +381,18 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor } } -bool InstStrategyAutoGenTriggers::hasUserPatterns( Node f ) { - if( f.getNumChildren()==3 ){ - std::map< Node, bool >::iterator it = d_hasUserPatterns.find( f ); +bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) { + if( q.getNumChildren()==3 ){ + std::map< Node, bool >::iterator it = d_hasUserPatterns.find( q ); if( it==d_hasUserPatterns.end() ){ bool hasPat = false; - for( unsigned i=0; i<f[2].getNumChildren(); i++ ){ - if( f[2][i].getKind()==INST_PATTERN ){ + for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ + if( q[2][i].getKind()==INST_PATTERN ){ hasPat = true; break; } } - d_hasUserPatterns[f] = hasPat; + d_hasUserPatterns[q] = hasPat; return hasPat; }else{ return it->second; @@ -407,11 +402,11 @@ bool InstStrategyAutoGenTriggers::hasUserPatterns( Node f ) { } } -void InstStrategyAutoGenTriggers::addUserNoPattern( Node f, Node pat ) { +void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) { Assert( pat.getKind()==INST_NO_PATTERN && pat.getNumChildren()==1 ); - if( std::find( d_user_no_gen[f].begin(), d_user_no_gen[f].end(), pat[0] )==d_user_no_gen[f].end() ){ - Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << f << std::endl; - d_user_no_gen[f].push_back( pat[0] ); + if( std::find( d_user_no_gen[q].begin(), d_user_no_gen[q].end(), pat[0] )==d_user_no_gen[q].end() ){ + Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << q << std::endl; + d_user_no_gen[q].push_back( pat[0] ); } } @@ -493,7 +488,7 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) { for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ - if( process( q, e ) ){ + if( process( q, e, quant_e ) ){ //added lemma addedLemmas++; } @@ -507,101 +502,110 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) { } } -bool FullSaturation::process( Node f, Theory::Effort effort ){ +bool FullSaturation::process( Node f, Theory::Effort effort, unsigned quant_e ){ //first, try from relevant domain RelevantDomain * rd = d_quantEngine->getRelevantDomain(); unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; - for( unsigned r=rstart; r<2; r++ ){ - if( rd || r>0 ){ - if( r==0 ){ - Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl; - }else{ - Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl; + unsigned rend = quant_e==QuantifiersEngine::QEFFORT_STANDARD ? rstart : 2; + for( unsigned r=rstart; r<=rend; r++ ){ + if( r==1 ){ + //complete guess + if( d_guessed.find( f )==d_guessed.end() ){ + Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl; + d_guessed[f] = true; + InstMatch m( f ); + if( d_quantEngine->addInstantiation( f, m ) ){ + ++(d_quantEngine->d_statistics.d_instantiations_guess); + return true; + } } - rd->compute(); - unsigned final_max_i = 0; - std::vector< unsigned > maxs; - for(unsigned i=0; i<f[0].getNumChildren(); i++ ){ - unsigned ts; + }else{ + if( rd || r>0 ){ if( r==0 ){ - ts = rd->getRDomain( f, i )->d_terms.size(); + Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl; }else{ - ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size(); + Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl; + } + rd->compute(); + bool max_zero = false; + unsigned final_max_i = 0; + std::vector< unsigned > maxs; + for(unsigned i=0; i<f[0].getNumChildren(); i++ ){ + unsigned ts; + if( r==0 ){ + ts = rd->getRDomain( f, i )->d_terms.size(); + }else{ + ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size(); + } + maxs.push_back( ts ); + Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl; + if( ts>final_max_i ){ + final_max_i = ts; + } + if( ts==0 ){ + max_zero = true; + } } - maxs.push_back( ts ); - Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl; - if( ts>final_max_i ){ - final_max_i = ts; + if( max_zero ){ + final_max_i = 0; } - } - Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl; + Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl; - unsigned max_i = 0; - bool success; - while( max_i<=final_max_i ){ - Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl; - std::vector< unsigned > childIndex; - int index = 0; - do { - while( index>=0 && index<(int)f[0].getNumChildren() ){ - if( index==(int)childIndex.size() ){ - childIndex.push_back( -1 ); - }else{ - Assert( index==(int)(childIndex.size())-1 ); - unsigned nv = childIndex[index]+1; - if( options::cbqi() ){ - //skip inst constant nodes - while( nv<maxs[index] && nv<=max_i && - r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){ - nv++; - } - } - if( nv<maxs[index] && nv<=max_i ){ - childIndex[index] = nv; - index++; + unsigned max_i = 0; + bool success; + while( max_i<=final_max_i ){ + Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl; + std::vector< unsigned > childIndex; + int index = 0; + do { + while( index>=0 && index<(int)f[0].getNumChildren() ){ + if( index==(int)childIndex.size() ){ + childIndex.push_back( -1 ); }else{ - childIndex.pop_back(); - index--; + Assert( index==(int)(childIndex.size())-1 ); + unsigned nv = childIndex[index]+1; + if( options::cbqi() ){ + //skip inst constant nodes + while( nv<maxs[index] && nv<=max_i && + r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){ + nv++; + } + } + if( nv<maxs[index] && nv<=max_i ){ + childIndex[index] = nv; + index++; + }else{ + childIndex.pop_back(); + index--; + } } } - } - success = index>=0; - if( success ){ - Trace("inst-alg-rd") << "Try instantiation { "; - for( unsigned j=0; j<childIndex.size(); j++ ){ - Trace("inst-alg-rd") << childIndex[j] << " "; - } - Trace("inst-alg-rd") << "}" << std::endl; - //try instantiation - std::vector< Node > terms; - for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ - if( r==0 ){ - terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] ); + success = index>=0; + if( success ){ + Trace("inst-alg-rd") << "Try instantiation { "; + for( unsigned j=0; j<childIndex.size(); j++ ){ + Trace("inst-alg-rd") << childIndex[j] << " "; + } + Trace("inst-alg-rd") << "}" << std::endl; + //try instantiation + std::vector< Node > terms; + for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ + if( r==0 ){ + terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] ); + }else{ + terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] ); + } + } + if( d_quantEngine->addInstantiation( f, terms, false ) ){ + Trace("inst-alg-rd") << "Success!" << std::endl; + ++(d_quantEngine->d_statistics.d_instantiations_guess); + return true; }else{ - terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] ); + index--; } } - if( d_quantEngine->addInstantiation( f, terms, false ) ){ - Trace("inst-alg-rd") << "Success!" << std::endl; - ++(d_quantEngine->d_statistics.d_instantiations_guess); - return true; - }else{ - index--; - } - } - }while( success ); - max_i++; - } - } - if( r==0 ){ - //complete guess - if( d_guessed.find( f )==d_guessed.end() ){ - Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl; - d_guessed[f] = true; - InstMatch m( f ); - if( d_quantEngine->addInstantiation( f, m ) ){ - ++(d_quantEngine->d_statistics.d_instantiations_guess); - return true; + }while( success ); + max_i++; } } } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index f02339e2e..e9eed800e 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -49,11 +49,11 @@ public: ~InstStrategyUserPatterns(){} public: /** add pattern */ - void addUserPattern( Node f, Node pat ); + void addUserPattern( Node q, Node pat ); /** get num patterns */ - int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); } + int getNumUserGenerators( Node q ) { return (int)d_user_gen[q].size(); } /** get user pattern */ - inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; } + inst::Trigger* getUserGenerator( Node q, int i ) { return d_user_gen[q][ i ]; } /** identify */ std::string identify() const { return std::string("UserPatterns"); } };/* class InstStrategyUserPatterns */ @@ -85,12 +85,12 @@ private: private: /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e ); + int process( Node q, Theory::Effort effort, int e ); /** generate triggers */ - void generateTriggers( Node f, Theory::Effort effort, int e, int& status ); + void generateTriggers( Node q, Theory::Effort effort, int e, int& status ); //bool addTrigger( inst::Trigger * tr, Node f, unsigned r ); /** has user patterns */ - bool hasUserPatterns( Node f ); + bool hasUserPatterns( Node q ); /** has user patterns */ std::map< Node, bool > d_hasUserPatterns; public: @@ -98,11 +98,11 @@ public: ~InstStrategyAutoGenTriggers(){} public: /** get auto-generated trigger */ - inst::Trigger* getAutoGenTrigger( Node f ); + inst::Trigger* getAutoGenTrigger( Node q ); /** identify */ std::string identify() const { return std::string("AutoGenTriggers"); } /** add pattern */ - void addUserNoPattern( Node f, Node pat ); + void addUserNoPattern( Node q, Node pat ); };/* class InstStrategyAutoGenTriggers */ class FullSaturation : public QuantifiersModule { @@ -110,7 +110,7 @@ private: /** guessed instantiations */ std::map< Node, bool > d_guessed; /** process functions */ - bool process( Node f, Theory::Effort effort ); + bool process( Node q, Theory::Effort effort, unsigned quant_e ); public: FullSaturation( QuantifiersEngine* qe ); ~FullSaturation(){} diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 49f561234..16cecb657 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -100,7 +100,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ if( !d_quantEngine->hasAddedLemma() ){ return false; }else{ - Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->d_lemmas_waiting.size()-lastWaiting) << std::endl; + Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; return true; } } @@ -186,14 +186,14 @@ void InstantiationEngine::registerQuantifier( Node f ){ } } -void InstantiationEngine::addUserPattern( Node f, Node pat ){ +void InstantiationEngine::addUserPattern( Node q, Node pat ){ if( d_isup ){ - d_isup->addUserPattern( f, pat ); + d_isup->addUserPattern( q, pat ); } } -void InstantiationEngine::addUserNoPattern( Node f, Node pat ){ +void InstantiationEngine::addUserNoPattern( Node q, Node pat ){ if( d_i_ag ){ - d_i_ag->addUserNoPattern( f, pat ); + d_i_ag->addUserNoPattern( q, pat ); } } diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 4a990ff6b..bfa610369 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -82,8 +82,8 @@ public: void registerQuantifier( Node q ); Node explain(TNode n){ return Node::null(); } /** add user pattern */ - void addUserPattern( Node f, Node pat ); - void addUserNoPattern( Node f, Node pat ); + void addUserPattern( Node q, Node pat ); + void addUserNoPattern( Node q, Node pat ); public: /** Identify this module */ std::string identify() const { return "InstEngine"; } diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 2578d0b7f..d7b66d52d 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -55,6 +55,8 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false perform aggressive miniscoping for quantifiers option elimTautQuant --elim-taut-quant bool :default true eliminate tautological disjuncts of quantified formulas +option purifyQuant --purify-quant bool :default false + purify quantified formulas #### E-matching options @@ -241,7 +243,7 @@ option cbqiSat --cbqi-sat bool :read-write :default true answer sat when quantifiers are asserted with counterexample-based quantifier instantiation option cbqiModel --cbqi-model bool :read-write :default true guide instantiations by model values for counterexample-based quantifier instantiation -option cbqiAll --cbqi-all bool :default false +option cbqiAll --cbqi-all bool :read-write :default false apply counterexample-based instantiation to all quantified formulas option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false use integer infinity for vts in counterexample-based quantifier instantiation diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 0b212d696..d289e3938 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -79,7 +79,7 @@ bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) { it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second ); msum[it->first] = Rewriter::rewrite( r ); }else{ - msum[it->first] = negate( it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second ); + msum[it->first] = it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(-1) ) : negate( it->second ); } } return true; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 895408269..dcf58e692 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" #include "theory/datatypes/datatypes_rewriter.h" +#include "theory/quantifiers/trigger.h" using namespace std; using namespace CVC4; @@ -82,6 +83,16 @@ bool QuantifiersRewriter::isCube( Node n ){ } } +int QuantifiersRewriter::getPurifyId( Node n ){ + if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){ + return 1; + }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL ){ + return 0; + }else{ + return -1; + } +} + void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){ if( n.getKind()==OR ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ @@ -758,70 +769,106 @@ Node QuantifiersRewriter::computeProcessIte( Node body, Node ipl ){ return body; } +bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ) { + if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){ + return false; + }else{ + if( !var_parent.empty() ){ + std::map< Node, std::vector< int > >::iterator it = var_parent.find( v ); + if( it!=var_parent.end() ){ + Assert( !it->second.empty() ); + int id = getPurifyId( s ); + return it->second.size()==1 && it->second[0]==id; + } + } + return true; + } +} -Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ - Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl; - QuantPhaseReq qpr( body ); - std::vector< Node > vars; - std::vector< Node > subs; - for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ - //Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl; - if( it->first.getKind()==EQUAL ){ - if( it->second && options::varElimQuant() ){ - TypeNode types[2]; - for( int i=0; i<2; i++ ){ - types[i] = it->first[i].getType(); +bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vector< Node >& args, std::vector< Node >& vars, std::vector< Node >& subs, + std::map< Node, std::vector< int > >& var_parent ) { + if( lit.getKind()==EQUAL && pol ){ + for( unsigned i=0; i<2; i++ ){ + std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[i] ); + if( ita!=args.end() ){ + if( isVariableElim( lit[i], lit[1-i], var_parent ) ){ + vars.push_back( lit[i] ); + subs.push_back( lit[1-i] ); + args.erase( ita ); + return true; } - for( int i=0; i<2; i++ ){ - std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] ); + } + } + //for arithmetic, solve the equality + if( lit[0].getType().isReal() ){ + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( lit, msum ) ){ + for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ + std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first ); if( ita!=args.end() ){ - if( !TermDb::containsTerm( it->first[1-i], it->first[i] ) && types[1-i].isSubtypeOf( types[i] ) ){ - vars.push_back( it->first[i] ); - subs.push_back( it->first[1-i] ); + Node veq_c; + Node val; + int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL ); + if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, var_parent ) ){ + vars.push_back( itm->first ); + subs.push_back( val ); args.erase( ita ); - break; + return true; } } } - if( !vars.empty() ){ - break; - } } - }else if( it->first.getKind()==APPLY_TESTER ){ - if( options::dtVarExpandQuant() && it->second && it->first[0].getKind()==BOUND_VARIABLE ){ - Trace("var-elim-dt") << "Expand datatype variable based on : " << it->first << std::endl; - std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[0] ); - if( ita!=args.end() ){ - vars.push_back( it->first[0] ); - Expr testerExpr = it->first.getOperator().toExpr(); - int index = Datatype::indexOf( testerExpr ); - const Datatype& dt = Datatype::datatypeOf(testerExpr); - const DatatypeConstructor& c = dt[index]; - std::vector< Node > newChildren; - newChildren.push_back( Node::fromExpr( c.getConstructor() ) ); - std::vector< Node > newVars; - for( unsigned j=0; j<c.getNumArgs(); j++ ){ - TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() ); - tn = tn[1]; - Node v = NodeManager::currentNM()->mkBoundVar( tn ); - newChildren.push_back( v ); - newVars.push_back( v ); - } - subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) ); - Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl; - args.erase( ita ); - args.insert( args.end(), newVars.begin(), newVars.end() ); - } - } - }else if( it->first.getKind()==BOUND_VARIABLE ){ - if( options::varElimQuant() ){ - std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first ); - if( ita!=args.end() ){ - Trace("var-elim-bool") << "Variable eliminate : " << it->first << " in " << body << std::endl; - vars.push_back( it->first ); - subs.push_back( NodeManager::currentNM()->mkConst( it->second ) ); - args.erase( ita ); - } + } + }else if( lit.getKind()==APPLY_TESTER && pol && lit[0].getKind()==BOUND_VARIABLE ){ + Trace("var-elim-dt") << "Expand datatype variable based on : " << lit << std::endl; + std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[0] ); + if( ita!=args.end() ){ + vars.push_back( lit[0] ); + Expr testerExpr = lit.getOperator().toExpr(); + int index = Datatype::indexOf( testerExpr ); + const Datatype& dt = Datatype::datatypeOf(testerExpr); + const DatatypeConstructor& c = dt[index]; + std::vector< Node > newChildren; + newChildren.push_back( Node::fromExpr( c.getConstructor() ) ); + std::vector< Node > newVars; + for( unsigned j=0; j<c.getNumArgs(); j++ ){ + TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() ); + tn = tn[1]; + Node v = NodeManager::currentNM()->mkBoundVar( tn ); + newChildren.push_back( v ); + newVars.push_back( v ); + } + subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) ); + Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl; + args.erase( ita ); + args.insert( args.end(), newVars.begin(), newVars.end() ); + return true; + } + }else if( lit.getKind()==BOUND_VARIABLE ){ + std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit ); + if( ita!=args.end() ){ + Trace("var-elim-bool") << "Variable eliminate : " << lit << std::endl; + vars.push_back( lit ); + subs.push_back( NodeManager::currentNM()->mkConst( pol ) ); + args.erase( ita ); + return true; + } + } + return false; +} + +Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, Node& ipl, std::map< Node, std::vector< int > >& var_parent ){ + Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl; + QuantPhaseReq qpr( body ); + std::vector< Node > vars; + std::vector< Node > subs; + for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ + //Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl; + if( ( it->first.getKind()==EQUAL && it->second && options::varElimQuant() ) || + ( it->first.getKind()==APPLY_TESTER && it->second && it->first[0].getKind()==BOUND_VARIABLE && options::dtVarExpandQuant() ) || + ( it->first.getKind()==BOUND_VARIABLE && options::varElimQuant() ) ){ + if( computeVariableElimLit( it->first, it->second, args, vars, subs, var_parent ) ){ + break; } } } @@ -838,6 +885,22 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& return body; } +Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ + //the parent id's for each variable, if using purifyQuant + std::map< Node, std::vector< int > > var_parent; + if( options::purifyQuant() ){ + body = computePurify( body, args, var_parent ); + } + if( options::varElimQuant() || options::dtVarExpandQuant() ){ + Node prev; + do{ + prev = body; + body = computeVarElimination2( body, args, ipl, var_parent ); + }while( prev!=body && !args.empty() ); + } + return body; +} + Node QuantifiersRewriter::computeClause( Node n ){ Assert( isClause( n ) ); if( isLiteral( n ) ){ @@ -1348,7 +1411,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ - return options::varElimQuant() || options::dtVarExpandQuant(); + return options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant(); //}else if( computeOption==COMPUTE_CNF ){ // return options::cnfQuant(); }else{ @@ -1394,11 +1457,7 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp }else if( computeOption==COMPUTE_PRENEX ){ n = computePrenex( n, args, true ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ - Node prev; - do{ - prev = n; - n = computeVarElimination( n, args, ipl ); - }while( prev!=n && !args.empty() ); + n = computeVarElimination( n, args, ipl ); //}else if( computeOption==COMPUTE_CNF ){ //n = computeCNF( n, args, defs, false ); //ipl = Node::null(); @@ -1620,3 +1679,83 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v } return n; } + + +Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term, + std::map< Node, std::vector< int > >& var_parent, int parentId ){ + std::map< Node, Node >::iterator it = visited.find( body ); + if( it!=visited.end() ){ + return it->second; + }else{ + Node ret = body; + if( body.getNumChildren()>0 && body.getKind()!=FORALL ){ + std::vector< Node > children; + bool childrenChanged = false; + int id = getPurifyId( body ); + for( unsigned i=0; i<body.getNumChildren(); i++ ){ + Node bi = computePurify2( body[i], args, visited, var_to_term, var_parent, id ); + childrenChanged = childrenChanged || bi!=body[i]; + children.push_back( bi ); + if( id!=0 && bi.getKind()==BOUND_VARIABLE ){ + if( std::find( var_parent[bi].begin(), var_parent[bi].end(), id )==var_parent[bi].end() ){ + var_parent[bi].push_back( id ); + } + } + } + if( childrenChanged ){ + if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.insert( children.begin(), body.getOperator() ); + } + ret = NodeManager::currentNM()->mkNode( body.getKind(), children ); + } + if( parentId!=0 && parentId!=id ){ + //must purify if this has a bound variable + if( TermDb::containsTerms( ret, args ) ){ + Node v = NodeManager::currentNM()->mkBoundVar( ret.getType() ); + var_to_term[v] = Rewriter::rewrite( v.eqNode( ret ) ); + ret = v; + args.push_back( v ); + } + } + } + visited[body] = ret; + return ret; + } +} + +Node QuantifiersRewriter::computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ) { + std::map< Node, Node > visited; + std::map< Node, Node > var_to_term; + Node pbody = computePurify2( body, args, visited, var_to_term, var_parent, 0 ); + if( pbody==body ){ + return body; + }else{ + Trace("quantifiers-rewrite-purify") << "Purify : " << body << std::endl; + Trace("quantifiers-rewrite-purify") << " Got : " << pbody << std::endl; + for( std::map< Node, Node >::iterator it = var_to_term.begin(); it != var_to_term.end(); ++it ){ + Trace("quantifiers-rewrite-purify") << " " << it->first << " : " << it->second << std::endl; + } + Trace("quantifiers-rewrite-purify") << "Variable parents : " << std::endl; + for( std::map< Node, std::vector< int > >::iterator it = var_parent.begin(); it != var_parent.end(); ++it ){ + Trace("quantifiers-rewrite-purify") << " " << it->first << " -> "; + for( unsigned i=0; i<it->second.size(); i++ ){ + Trace("quantifiers-rewrite-purify") << it->second[i] << " "; + } + Trace("quantifiers-rewrite-purify") << std::endl; + } + Trace("quantifiers-rewrite-purify") << std::endl; + std::vector< Node > disj; + for( std::map< Node, Node >::iterator it = var_to_term.begin(); it != var_to_term.end(); ++it ){ + disj.push_back( it->second.negate() ); + } + Node res; + if( disj.empty() ){ + res = pbody; + }else{ + disj.push_back( pbody ); + res = NodeManager::currentNM()->mkNode( OR, disj ); + } + Trace("quantifiers-rewrite-purify") << "Constructed : " << res << std::endl << std::endl; + return res; + } +} diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 0ad79587a..daf5a8bad 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -31,6 +31,7 @@ public: static bool isClause( Node n ); static bool isLiteral( Node n ); static bool isCube( Node n ); + static int getPurifyId( Node n ); private: static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); static Node mkForAll( std::vector< Node >& args, Node body, Node ipl ); @@ -40,6 +41,12 @@ private: static Node computeClause( Node n ); static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); static bool isConditionalVariableElim( Node n, int pol=0 ); + static bool isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ); + static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs, + std::map< Node, std::vector< int > >& var_parent ); + static Node computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term, + std::map< Node, std::vector< int > >& var_parent, int parentId ); + static Node computeVarElimination2( Node body, std::vector< Node >& args, Node& ipl, std::map< Node, std::vector< int > >& var_parent ); private: static Node computeElimSymbols( Node body ); static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ); @@ -50,10 +57,11 @@ private: std::map< Node, Node >& cache, std::map< Node, Node >& icache, std::vector< Node >& new_vars, std::vector< Node >& new_conds ); static Node computeProcessIte( Node body, Node ipl ); - static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); static Node computeSplit( Node f, std::vector< Node >& args, Node body ); + static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); + static Node computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ); private: enum{ COMPUTE_ELIM_SYMBOLS = 0, diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index e513666a4..e41af5e2d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -699,19 +699,6 @@ bool TermDb::hasInstConstAttr( Node n ) { return !getInstConstAttr(n).isNull(); } -void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) { - if (n.getKind()==BOUND_VARIABLE ){ - if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){ - bvs.push_back( n ); - } - }else{ - for( unsigned i=0; i<n.getNumChildren(); i++) { - getBoundVars(n[i], bvs); - } - } -} - - /** get the i^th instantiation constant of q */ Node TermDb::getInstantiationConstant( Node q, int i ) const { std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index bc8851195..f809aa5b8 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -262,10 +262,6 @@ public: static Node getInstConstAttr( Node n ); static bool hasInstConstAttr( Node n ); -//for bound variables -public: - //get bound variables in n - static void getBoundVars( Node n, std::vector< Node >& bvs ); //for skolem diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index de3c503b5..1f332e909 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -212,11 +212,11 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOpt return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers ); } -bool Trigger::isUsable( Node n, Node f ){ - if( quantifiers::TermDb::getInstConstAttr(n)==f ){ +bool Trigger::isUsable( Node n, Node q ){ + if( quantifiers::TermDb::getInstConstAttr(n)==q ){ if( isAtomicTrigger( n ) ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( !isUsable( n[i], f ) ){ + if( !isUsable( n[i], q ) ){ return false; } } @@ -227,8 +227,7 @@ bool Trigger::isUsable( Node n, Node f ){ std::map< Node, Node > coeffs; if( isBooleanTermTrigger( n ) ){ return true; - } - if( options::purifyTriggers() ){ + }else if( options::purifyTriggers() ){ Node x = getInversionVariable( n ); if( !x.isNull() ){ return true; @@ -241,41 +240,39 @@ bool Trigger::isUsable( Node n, Node f ){ } } -bool nodeContainsVar( Node n, Node v ){ - if( n==v) { - return true; - }else{ - for( unsigned i=0; i<n.getNumChildren(); i++) { - if( nodeContainsVar(n[i], v) ){ - return true; - } - } - return false; - } -} - Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl; + if( n.getKind()==NOT ){ + pol = !pol; + n = n[0]; + } if( options::relationalTriggers() ){ if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){ Node rtr; + bool do_negate = hasPol && pol; for( unsigned i=0; i<2; i++) { - unsigned j = (i==0) ? 1 : 0; - if( n[j].getKind()==INST_CONSTANT && isUsableTrigger(n[i], f) && !nodeContainsVar( n[i], n[j] ) ) { - rtr = n; - break; + if( n[1-i].getKind()==INST_CONSTANT ){ + if( isUsableTrigger(n[i], f) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) ){ + rtr = n; + break; + } + if( n[i].getKind()==INST_CONSTANT && ( !hasPol || pol ) ){ + do_negate = true; + rtr = n; + break; + } } } if( n[0].getType().isInteger() ){ //try to rearrange? std::map< Node, Node > m; - if (QuantArith::getMonomialSumLit(n, m) ){ + if( QuantArith::getMonomialSumLit(n, m) ){ for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){ if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){ Node veq; if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){ int vti = veq[0]==it->first ? 1 : 0; - if( isUsableTrigger(veq[vti], f) && !nodeContainsVar( veq[vti], veq[vti==0 ? 1 : 0]) ){ + if( isUsableTrigger( veq[vti], f ) && !quantifiers::TermDb::containsTerm( veq[vti], veq[1-vti] ) ){ rtr = veq; } } @@ -290,7 +287,8 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { if( hasPol ){ Trace("relational-trigger") << " polarity : " << pol << std::endl; } - Node rtr2 = (hasPol && pol) ? rtr.negate() : rtr; + Node rtr2 = do_negate ? rtr.negate() : rtr; + Trace("relational-trigger") << " return : " << rtr2 << std::endl; return rtr2; } } @@ -304,8 +302,8 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { } } -bool Trigger::isUsableTrigger( Node n, Node f ){ - Node nu = getIsUsableTrigger(n,f); +bool Trigger::isUsableTrigger( Node n, Node q ){ + Node nu = getIsUsableTrigger( n, q ); return !nu.isNull(); } @@ -346,16 +344,15 @@ bool Trigger::isSimpleTrigger( Node n ){ bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){ if( patMap.find( n )==patMap.end() ){ patMap[ n ] = false; - bool newHasPol = n.getKind()==IFF ? false : hasPol; - bool newPol = n.getKind()==NOT ? !pol : pol; if( tstrt==TS_MIN_TRIGGER ){ if( n.getKind()==FORALL ){ return false; }else{ bool retVal = false; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; - if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + bool newHasPol, newPol; + QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); + if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol ) ){ retVal = true; } } @@ -389,9 +386,10 @@ bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, } } if( n.getKind()!=FORALL ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; - if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + bool newHasPol, newPol; + QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); + if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol ) ){ retVal = true; } } @@ -558,13 +556,19 @@ Node Trigger::getInversion( Node n, Node x ) { }else if( n.getKind()==MULT ){ Assert( n[i].isConst() ); if( x.getType().isInteger() ){ - Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>() ); - x = NodeManager::currentNM()->mkNode( INTS_DIVISION, x, coeff ); + Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>().abs() ); + if( !n[i].getConst<Rational>().abs().isOne() ){ + x = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, x, coeff ); + } + if( n[i].getConst<Rational>().sgn()<0 ){ + x = NodeManager::currentNM()->mkNode( UMINUS, x ); + } }else{ Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() ); x = NodeManager::currentNM()->mkNode( MULT, x, coeff ); } } + x = Rewriter::rewrite( x ); }else{ Assert( cindex==-1 ); cindex = i; diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 1817ebe56..11962008e 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -91,7 +91,7 @@ public: bool smartTriggers = false ); private: /** is subterm of trigger usable */ - static bool isUsable( Node n, Node f ); + static bool isUsable( Node n, Node q ); static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false ); /** collect all APPLY_UF pattern terms for f in n */ static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ); @@ -105,7 +105,7 @@ public: static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst = false ); public: /** is usable trigger */ - static bool isUsableTrigger( Node n, Node f ); + static bool isUsableTrigger( Node n, Node q ); static bool isAtomicTrigger( Node n ); static bool isAtomicTriggerKind( Kind k ); static bool isCbqiKind( Kind k ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index aab04c32c..990d3389e 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -901,7 +901,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo Assert( terms.size()==q[0].getNumChildren() ); Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl; for( unsigned i=0; i<terms.size(); i++ ){ - Trace("inst-add-debug") << " " << q[0][i] << " -> " << terms[i]; + Trace("inst-add-debug") << " " << q[0][i] << " -> " << terms[i] << std::endl; //make it representative, this is helpful for recognizing duplication if( mkRep ){ //pick the best possible representative for instantiation, based on past use and simplicity of term @@ -910,7 +910,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo //ensure the type is correct terms[i] = quantifiers::TermDb::mkNodeType( terms[i], q[0][i].getType() ); } - Trace("inst-add-debug") << " -> " << terms[i] << std::endl; + Trace("inst-add-debug2") << " -> " << terms[i] << std::endl; Assert( !terms[i].isNull() ); } diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 138fb4bb0..a53759c08 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -334,6 +334,20 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { } } +Expr getSubtermWithType( Expr e, Type t, bool isTop ){ + if( !isTop && e.getType()==t ){ + return e; + }else{ + for( unsigned i=0; i<e.getNumChildren(); i++ ){ + Expr se = getSubtermWithType( e[i], t, false ); + if( !se.isNull() ){ + return se; + } + } + return Expr(); + } +} + Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) { if( std::find( processing.begin(), processing.end(), d_self )==processing.end() ){ processing.push_back( d_self ); @@ -342,8 +356,14 @@ Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) cons //do nullary constructors first if( ((*i).getNumArgs()==0)==(r==0)){ Debug("datatypes") << "Try constructing for " << (*i).getName() << ", processing = " << processing.size() << std::endl; - Expr e = (*i).computeGroundTerm( t, processing ); + Expr e = (*i).computeGroundTerm( t, processing, d_ground_term ); if( !e.isNull() ){ + //must check subterms for the same type to avoid infinite loops in type enumeration + Expr se = getSubtermWithType( e, t, true ); + if( !se.isNull() ){ + Debug("datatypes") << "Take subterm " << se << std::endl; + e = se; + } processing.pop_back(); return e; }else{ @@ -780,7 +800,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { return true; } -Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) { +Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException) { // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_constructor); @@ -801,8 +821,13 @@ Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& proces } Expr arg; if( selType.isDatatype() ){ - const Datatype & dt = DatatypeType(selType).getDatatype(); - arg = dt.computeGroundTerm( selType, processing ); + std::map< Type, Expr >::iterator itgt = gt.find( selType ); + if( itgt != gt.end() ){ + arg = itgt->second; + }else{ + const Datatype & dt = DatatypeType(selType).getDatatype(); + arg = dt.computeGroundTerm( selType, processing ); + } }else{ arg = selType.mkGroundTerm(); } diff --git a/src/util/datatype.h b/src/util/datatype.h index 0b8b8c61f..85668cd55 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -218,7 +218,7 @@ private: /** compute whether this datatype is well-founded */ bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException); /** compute ground term */ - Expr computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException); + Expr computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException); public: /** * Create a new Datatype constructor with the given name for the diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 45a9d6f30..d06fb1b9b 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -67,7 +67,8 @@ TESTS = \ manos-model.smt2 \ bug625.smt2 \ cdt-model-cade15.smt2 \ - sc-cdt1.smt2 + sc-cdt1.smt2 \ + conqueue-dt-enum-iloop.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 new file mode 100644 index 000000000..6f82cd842 --- /dev/null +++ b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 @@ -0,0 +1,75 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-fun start!13 () Bool) + +(assert start!13) + +(declare-fun b!39 () Bool) + +(declare-sort T!14 0) + +(declare-datatypes () ( +(LazyConQ!5 + (Lazyarg1!5 (carry!37 Conc!6) (srear!9 LazyConQ!5)) + (Lazyarg2!5 (t!270 ConQ!6)) + (Lazyarg3!5 (carry!38 Conc!6) (t!271 ConQ!6)) + (Lazyarg4!5 (tree!19 Conc!6) (carry!39 Conc!6)) + (Lazyarg5!5 (tree!20 Conc!6) (carry!40 Conc!6)) + (PushLeft!5 (ys!22 Conc!6) (xs!60 LazyConQ!5)) + (PushLeftLazy!5 (ys!23 Conc!6) (xs!61 LazyConQ!5))) +(Conc!6 + (CC!5 (left!9 Conc!6) (right!9 Conc!6)) + (Empty!5) + (Single!5 (x!106 T!14))) +(ConQ!6 + (Spine!5 (head!10 Conc!6) (rear!5 LazyConQ!5)) + (Tip!5 (t!272 Conc!6))) +)) + +(declare-fun e!41 () LazyConQ!5) + +(declare-fun l!2 () LazyConQ!5) + +(declare-fun st!3 () (Set LazyConQ!5)) + +(declare-fun firstUnevaluated!3 (LazyConQ!5 (Set LazyConQ!5)) LazyConQ!5) + +(declare-fun evalLazyConQ2!7 (LazyConQ!5) ConQ!6) + +(assert (=> b!39 (= e!41 (firstUnevaluated!3 (rear!5 (evalLazyConQ2!7 l!2)) st!3)))) + +(declare-fun b!40 () Bool) + +(declare-fun e!42 () LazyConQ!5) + +(assert (=> b!40 (= e!42 e!41))) + +(assert (=> b!40 (= b!39 (is-Spine!5 (evalLazyConQ2!7 l!2))))) + +(declare-fun b!41 () Bool) + +(assert (=> b!40 (or (not b!39) (not b!41)))) + +(assert (=> b!40 (or b!39 b!41))) + +(assert (=> b!41 (= e!41 l!2))) + +(declare-fun b!42 () Bool) + +(assert (=> b!42 (= e!42 l!2))) + +(declare-fun lt!14 () LazyConQ!5) + +(declare-fun isTip!5 (ConQ!6) Bool) + +(assert (=> start!13 (and (not (isTip!5 (evalLazyConQ2!7 lt!14))) (member lt!14 st!3)))) + +(assert (=> start!13 (= lt!14 e!42))) + +(assert (=> start!13 (= b!40 (member l!2 st!3)))) + +(assert (=> start!13 (or (not b!40) (not b!42)))) + +(assert (=> start!13 (or b!40 b!42))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index e6b0a59fc..939b0d22c 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -61,7 +61,9 @@ TESTS = \ mix-simp.smt2 \ mix-coeff.smt2 \ mix-match.smt2 \ - ari056.smt2 + ari056.smt2 \ + ext-ex-deq-trigger.smt2 \ + matching-lia-1arg.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 b/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 new file mode 100644 index 000000000..f6f96fe02 --- /dev/null +++ b/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --relational-triggers +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-sort U 0) + +(declare-const k U) +(declare-const ff U) +(declare-const ffk U) +(declare-fun fun1 (Int) Int) +(declare-fun fun2 (Int) Int) +(declare-fun c (U U) U) +(declare-fun app (U Int) Int) + +(assert (forall ((f U) (g U)) (=> (forall ((x Int)) (= (app f x) (app g x))) (= f g)) )) + +(assert (forall ((x Int)) (= (app ff x) (+ (fun1 x) (fun2 x))))) +(assert (forall ((x Int)) (= (app ffk x) (+ (fun1 (app k x)) (fun2 (app k x)))))) + +(assert (forall ((f U) (g U) (x Int)) (= (app (c f g) x) (app f (app g x))))) + +(assert (not (= (c ff k) ffk))) + +(check-sat) + diff --git a/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 b/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 new file mode 100644 index 000000000..aaf9b2c1f --- /dev/null +++ b/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --purify-triggers +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(declare-fun P (Int) Bool) +(assert (forall ((x Int)) (P (* 2 x)))) +(assert (not (P 38))) +(check-sat) + diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index a1f91a6ce..71ca64aea 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -45,7 +45,8 @@ TESTS = commutative.sy \ sygus-dt.sy \ dt-no-syntax.sy \ list-head-x.sy \ - clock-inc-tuple.sy + clock-inc-tuple.sy \ + dt-test-ns.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/dt-test-ns.sy b/test/regress/regress0/sygus/dt-test-ns.sy new file mode 100644 index 000000000..ed17f4ff2 --- /dev/null +++ b/test/regress/regress0/sygus/dt-test-ns.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si --no-dump-synth +(set-logic LIA) + +(declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) + +(synth-fun f ((x Int)) List) + +(declare-var x Int) + +(constraint (is-cons (f x))) +(constraint (and (= (head (f x)) x) (= (head (f x)) (+ 5 (head (tail (f x))))))) +(check-synth) + |