From 73cecf65a750b9ee59486083af5ee55734da0a6a Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 24 Jan 2015 19:00:59 +0100 Subject: [PATCH] Add --lte-restrict-inst-closure option. Push dt.size fairness constraints inside splitting lemmas for sygus. --- src/theory/datatypes/datatypes_sygus.cpp | 252 ++++++++++-------- src/theory/datatypes/theory_datatypes.cpp | 61 +++-- src/theory/quantifiers/options | 2 + src/theory/quantifiers/term_database.cpp | 37 ++- src/theory/quantifiers/term_database.h | 21 +- src/theory/quantifiers/theory_quantifiers.cpp | 3 + src/theory/quantifiers_engine.cpp | 46 ++-- 7 files changed, 247 insertions(+), 175 deletions(-) diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index c7b3e69c4..ee8169db7 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -110,6 +110,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > Node arg1; Kind parentKind = UNDEFINED_KIND; TypeNode tnnp; + Node ptest; if( n.getKind()==APPLY_SELECTOR_TOTAL ){ Node op = n.getOperator(); Expr selectorExpr = op.toExpr(); @@ -133,13 +134,13 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > } } } - + // we are splitting on a term that may later have no semantics : guard this case - Node ptest = DatatypesRewriter::mkTester( n[0], csIndex, pdt ).negate(); + ptest = DatatypesRewriter::mkTester( n[0], csIndex, pdt ); Trace("sygus-split-debug") << "Parent guard : " << ptest << std::endl; - d_splits[n].push_back( ptest ); } - + std::vector< Node > ptest_c; + bool narrow = false; for( unsigned i=0; i } if( addSplit ){ Node test = DatatypesRewriter::mkTester( n, i, dt ); - + //check if we can strengthen the first argument if( !arg1.isNull() ){ std::map< int, std::vector< int > >::iterator it = d_sygus_pc_arg_pos[tnn][csIndex].find( i ); @@ -164,24 +165,48 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > Node argStr = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( OR, lem_c ); Trace("sygus-str") << "...strengthen corresponding first argument of " << test << " : " << argStr << std::endl; test = NodeManager::currentNM()->mkNode( AND, test, argStr ); + narrow = true; } } + //add fairness constraint + if( options::ceGuidedInstFair()==quantifiers::CEGQI_FAIR_DT_SIZE ){ + Node szl = NodeManager::currentNM()->mkNode( DT_SIZE, n ); + Node szr = NodeManager::currentNM()->mkNode( DT_SIZE, DatatypesRewriter::getInstCons( n, dt, i ) ); + szr = Rewriter::rewrite( szr ); + test = NodeManager::currentNM()->mkNode( AND, test, szl.eqNode( szr ) ); + } d_splits[n].push_back( test ); Trace("sygus-split-debug2") << "SUCCESS" << std::endl; Trace("sygus-split") << "Disjunct #" << d_splits[n].size() << " : " << test << std::endl; }else{ Trace("sygus-split-debug2") << "redundant argument" << std::endl; + narrow = true; } }else{ Trace("sygus-split-debug2") << "redundant operator" << std::endl; + narrow = true; + } + if( !ptest.isNull() ){ + ptest_c.push_back( DatatypesRewriter::mkTester( n, i, dt ) ); } } - if( d_splits[n].empty() ){ //possible - + exit( 3 ); + Assert( false ); } + if( narrow && !ptest.isNull() ){ + Node split = d_splits[n].size()==1 ? d_splits[n][0] : NodeManager::currentNM()->mkNode( OR, d_splits[n] ); + d_splits[n].clear(); + split = NodeManager::currentNM()->mkNode( AND, ptest, split ); + d_splits[n].push_back( split ); + if( !ptest_c.empty() ){ + ptest = NodeManager::currentNM()->mkNode( AND, ptest.negate(), NodeManager::currentNM()->mkNode( OR, ptest_c ) ); + } + d_splits[n].push_back( ptest ); + } + } //copy to splits splits.insert( splits.end(), d_splits[n].begin(), d_splits[n].end() ); @@ -213,33 +238,35 @@ void SygusSplit::registerSygusType( TypeNode tn, const Datatype& dt ) { //compute the redundant operators for( unsigned i=0; i::iterator it = d_arg_kind[tn].find( i ); - if( it!=d_arg_kind[tn].end() ){ - Kind dk; - if( isAntisymmetric( it->second, dk ) ){ - std::map< Kind, int >::iterator ita = d_kinds[tn].find( dk ); - if( ita!=d_kinds[tn].end() ){ - Trace("sygus-split-debug") << "Possible redundant operator : " << it->second << " with " << dk << std::endl; - //check for type mismatches - bool success = true; - unsigned j = ita->second; - for( unsigned k=0; k<2; k++ ){ - unsigned ko = k==0 ? 1 : 0; - TypeNode tni = TypeNode::fromType( ((SelectorType)dt[i][k].getType()).getRangeType() ); - TypeNode tnj = TypeNode::fromType( ((SelectorType)dt[j][ko].getType()).getRangeType() ); - if( tni!=tnj ){ - Trace("sygus-split-debug") << "Argument types " << tni << " and " << tnj << " are not equal." << std::endl; - success = false; - break; + if( options::sygusNormalForm() ){ + std::map< int, Kind >::iterator it = d_arg_kind[tn].find( i ); + if( it!=d_arg_kind[tn].end() ){ + Kind dk; + if( isAntisymmetric( it->second, dk ) ){ + std::map< Kind, int >::iterator ita = d_kinds[tn].find( dk ); + if( ita!=d_kinds[tn].end() ){ + Trace("sygus-split-debug") << "Possible redundant operator : " << it->second << " with " << dk << std::endl; + //check for type mismatches + bool success = true; + unsigned j = ita->second; + for( unsigned k=0; k<2; k++ ){ + unsigned ko = k==0 ? 1 : 0; + TypeNode tni = TypeNode::fromType( ((SelectorType)dt[i][k].getType()).getRangeType() ); + TypeNode tnj = TypeNode::fromType( ((SelectorType)dt[j][ko].getType()).getRangeType() ); + if( tni!=tnj ){ + Trace("sygus-split-debug") << "Argument types " << tni << " and " << tnj << " are not equal." << std::endl; + success = false; + break; + } + } + if( success ){ + Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << d_arg_kind[tn][i] << " terms." << std::endl; + nred = false; } - } - if( success ){ - Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << d_arg_kind[tn][i] << " terms." << std::endl; - nred = false; } } + //NAND,NOR } - //NAND,NOR } d_sygus_nred[tn].push_back( nred ); } @@ -251,85 +278,92 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& if( it==d_sygus_pc_nred[tnn][csIndex].end() ){ registerSygusType( tnnp, pdt ); Trace("sygus-split") << "Register type constructor arg " << dt.getName() << " " << csIndex << " " << sIndex << std::endl; - //get parent kind - bool hasParentKind = false; - Kind parentKind; - if( isKindArg( tnnp, csIndex ) ){ - hasParentKind = true; - parentKind = d_arg_kind[tnnp][csIndex]; - } - for( unsigned i=0; i rem_arg; - if( isComm( parentKind ) ){ - for( unsigned j=0; ji ){ - //based on commutativity - // use term ordering : constructor index of first argument is not greater than constructor index of second argument - rem_arg[j] = true; - }else{ - if( parentKind!=UNDEFINED_KIND && dt[i].getNumArgs()==0 && dt[j].getNumArgs()==0 ){ - Node nr = NodeManager::currentNM()->mkNode( parentKind, dt[j].getSygusOp(), dt[i].getSygusOp() ); - Node nrr = Rewriter::rewrite( nr ); - Trace("sygus-split-debug") << " Test constant args : " << nr << " rewrites to " << nrr << std::endl; - //based on rewriting - // if rewriting the two arguments gives an operator that is in the parent syntax, remove the redundancy - if( hasOp( tnnp, nrr ) ){ - Trace("sygus-nf") << "* Sygus norm : simplify based on rewrite " << nr << " -> " << nrr << std::endl; - rem_arg[j] = true; - } + //also compute argument relationships + if( options::sygusNormalFormArg() ){ + if( isKindArg( tnnp, csIndex ) && pdt[csIndex].getNumArgs()==2 ){ + int osIndex = sIndex==0 ? 1 : 0; + if( isArgDatatype( pdt[csIndex], osIndex, dt ) ){ + registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, osIndex ); + if( sIndex==0 ){ + Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() ); + Assert( d_sygus_pc_nred[tnn][csIndex].find( osIndex )!=d_sygus_pc_nred[tnn][csIndex].end() ); + + Kind parentKind = d_arg_kind[tnnp][csIndex]; + bool isPComm = isComm( parentKind ); + for( unsigned i=0; i rem_arg; + if( isComm( parentKind ) ){ + for( unsigned j=0; ji ){ + //based on commutativity + // use term ordering : constructor index of first argument is not greater than constructor index of second argument + rem_arg[j] = true; + }else{ + if( parentKind!=UNDEFINED_KIND && dt[i].getNumArgs()==0 && dt[j].getNumArgs()==0 ){ + Node nr = NodeManager::currentNM()->mkNode( parentKind, dt[j].getSygusOp(), dt[i].getSygusOp() ); + Node nrr = Rewriter::rewrite( nr ); + Trace("sygus-split-debug") << " Test constant args : " << nr << " rewrites to " << nrr << std::endl; + //based on rewriting + // if rewriting the two arguments gives an operator that is in the parent syntax, remove the redundancy + if( hasOp( tnnp, nrr ) ){ + Trace("sygus-nf") << "* Sygus norm : simplify based on rewrite " << nr << " -> " << nrr << std::endl; + rem_arg[j] = true; + } + } } } } } - } - if( !rem_arg.empty() ){ - d_sygus_pc_arg_pos[tnn][csIndex][i].clear(); - Trace("sygus-split-debug") << "Possibilities for first argument of " << parentKind << ", when second argument is " << dt[i].getName() << " : " << std::endl; - for( unsigned j=0; j reqk_arg; //TODO if( parent==NOT ){ - if( k==AND ) { + if( k==AND ) { nk = OR;reqk = NOT; - }else if( k==OR ){ + }else if( k==OR ){ nk = AND;reqk = NOT; - }else if( k==IFF ) { + }else if( k==IFF ) { nk = XOR; - }else if( k==XOR ) { + }else if( k==XOR ) { nk = IFF; } } if( parent==BITVECTOR_NOT ){ - if( k==BITVECTOR_AND ) { + if( k==BITVECTOR_AND ) { nk = BITVECTOR_OR;reqk = BITVECTOR_NOT; - }else if( k==BITVECTOR_OR ){ + }else if( k==BITVECTOR_OR ){ nk = BITVECTOR_AND;reqk = BITVECTOR_NOT; - }else if( k==BITVECTOR_XNOR ) { + }else if( k==BITVECTOR_XNOR ) { nk = BITVECTOR_XOR; - }else if( k==BITVECTOR_XOR ) { + }else if( k==BITVECTOR_XOR ) { nk = BITVECTOR_XNOR; } } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 501b3d86e..f9a451459 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -66,8 +66,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_true = NodeManager::currentNM()->mkConst( true ); d_dtfCounter = 0; - - if( options::sygusNormalForm() ){ + + if( options::ceGuidedInst() ){ d_sygus_split = new SygusSplit; }else{ d_sygus_split = NULL; @@ -360,6 +360,9 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){ doPendingMerges(); //add to tester if applicable if( atom.getKind()==kind::APPLY_TESTER ){ + if( polarity ){ + Trace("dt-tester") << "Assert tester : " << atom << std::endl; + } Node rep = getRepresentative( atom[0] ); EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); addTester( fact, eqc, rep ); @@ -1070,26 +1073,30 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { // r = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[s.getOperator().toExpr()], s[0] ); //}else{ r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c ); - }else if( s.getKind()==DT_SIZE ){ - r = NodeManager::currentNM()->mkNode( DT_SIZE, c ); - }else if( s.getKind()==DT_HEIGHT_BOUND ){ - r = NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, c, s[1] ); - if( r==d_true ){ - return; + }else{ + if( s.getKind()==DT_SIZE ){ + r = NodeManager::currentNM()->mkNode( DT_SIZE, c ); + }else if( s.getKind()==DT_HEIGHT_BOUND ){ + r = NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, c, s[1] ); + if( r==d_true ){ + return; + } } } - Node rr = Rewriter::rewrite( r ); - if( s!=rr ){ - Node eq_exp = c.eqNode( s[0] ); - Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr ); - Trace("datatypes-infer") << "DtInfer : collapse sel"; - Trace("datatypes-infer") << ( wrong ? " wrong" : ""); - Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl; + if( !r.isNull() ){ + Node rr = Rewriter::rewrite( r ); + if( s!=rr ){ + Node eq_exp = c.eqNode( s[0] ); + Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr ); + Trace("datatypes-infer") << "DtInfer : collapse sel"; + Trace("datatypes-infer") << ( wrong ? " wrong" : ""); + Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl; - d_pending.push_back( eq ); - d_pending_exp[ eq ] = eq_exp; - d_infer.push_back( eq ); - d_infer_exp.push_back( eq_exp ); + d_pending.push_back( eq ); + d_pending_exp[ eq ] = eq_exp; + d_infer.push_back( eq ); + d_infer_exp.push_back( eq_exp ); + } } } @@ -1116,8 +1123,8 @@ void TheoryDatatypes::computeCareGraph(){ for( unsigned j=i+1; jmkConst( Rational(0) ) ); std::vector< Node > children; @@ -1412,7 +1414,10 @@ void TheoryDatatypes::collectTerms( Node n ) { d_pending.push_back( conc ); d_pending_exp[ conc ] = d_true; d_infer.push_back( conc ); - }else if( n.getKind() == DT_HEIGHT_BOUND ){ +*/ + } + + if( n.getKind() == DT_HEIGHT_BOUND ){ if( n[1].getConst().isZero() ){ std::vector< Node > children; const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 560e29c3b..b47c98aa3 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -207,5 +207,7 @@ option localTheoryExt --local-t-ext bool :default false do instantiation based on local theory extensions option ltePartialInst --lte-partial-inst bool :default false partially instantiate local theory quantifiers +option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false + treat arguments of inst closure as restricted terms for instantiation endmodule diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 69271e021..fb28974a9 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -322,15 +322,19 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, return false; } -bool TermDb::hasTermCurrent( Node n ) { - //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE - if( options::termDbMode()==TERM_DB_ALL ){ - return true; - }else if( options::termDbMode()==TERM_DB_RELEVANT ){ +bool TermDb::hasTermCurrent( Node n, bool useMode ) { + if( !useMode ){ return d_has_map.find( n )!=d_has_map.end(); }else{ - Assert( false ); - return false; + //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE + if( options::termDbMode()==TERM_DB_ALL ){ + return true; + }else if( options::termDbMode()==TERM_DB_RELEVANT ){ + return d_has_map.find( n )!=d_has_map.end(); + }else{ + Assert( false ); + return false; + } } } @@ -364,7 +368,12 @@ Node TermDb::getHasTermEqc( Node r ) { } } +bool TermDb::isInstClosure( Node r ) { + return d_iclosure_processed.find( r )!=d_iclosure_processed.end(); +} + void TermDb::setHasTerm( Node n ) { + Trace("term-db-debug2") << "hasTerm : " << n << std::endl; //if( inst::Trigger::isAtomicTrigger( n ) ){ if( d_has_map.find( n )==d_has_map.end() ){ d_has_map[n] = true; @@ -391,9 +400,9 @@ void TermDb::reset( Theory::Effort effort ){ d_func_map_trie.clear(); d_func_map_eqc_trie.clear(); - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); //compute has map - if( options::termDbMode()==TERM_DB_RELEVANT ){ + if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){ d_has_map.clear(); d_has_eqc.clear(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); @@ -423,7 +432,9 @@ void TermDb::reset( Theory::Effort effort ){ if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) { context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); for (unsigned i = 0; it != it_end; ++ it, ++i) { - setHasTerm( (*it).assertion ); + if( (*it).assertion.getKind()!=INST_CLOSURE ){ + setHasTerm( (*it).assertion ); + } } } } @@ -443,7 +454,7 @@ void TermDb::reset( Theory::Effort effort ){ computeModelBasisArgAttribute( n ); } computeArgReps( n ); - + if( Trace.isOn("term-db-debug") ){ Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; for( unsigned i=0; ifirst ].addTerm( n, d_arg_reps[n] ) ){ NoMatchAttribute nma; n.setAttribute(nma,true); @@ -1157,7 +1168,7 @@ void TermDb::computeAttributes( Node q ) { //not necessarily nested existential //Assert( q[1].getKind()==NOT ); //Assert( q[1][0].getKind()==FORALL ); - + Trace("quant-attr") << "Attribute : sygus : " << q << std::endl; d_qattr_sygus[q] = true; if( d_quantEngine->getCegInstantiation()==NULL ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index f841bb2d8..8a20d6b41 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -33,7 +33,7 @@ typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute; /** Attribute true for quantifiers that are conjecture */ struct ConjectureAttributeId {}; typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute; - + /** Attribute true for function definition quantifiers */ struct FunDefAttributeId {}; typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute; @@ -183,10 +183,11 @@ public: /** is entailed (incomplete check) */ bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); /** has term */ - bool hasTermCurrent( Node n ); + bool hasTermCurrent( Node n, bool useMode = true ); /** get has term eqc */ Node getHasTermEqc( Node r ); - + /** is inst closure */ + bool isInstClosure( Node r ); //for model basis private: //map from types to model basis terms @@ -252,8 +253,8 @@ public: public: //get bound variables in n static void getBoundVars( Node n, std::vector< Node >& bvs); - - + + //for skolem private: /** map from universal quantifiers to their skolemized body */ @@ -268,9 +269,9 @@ public: Node getSkolemizedBody( Node f); /** is induction variable */ static bool isInductionTerm( Node n ); - + //for ground term enumeration -private: +private: /** ground terms enumerated for types */ std::map< TypeNode, std::vector< Node > > d_enum_terms; //type enumerators @@ -278,8 +279,8 @@ private: std::vector< TypeEnumerator > d_typ_enum; public: //get nth term for type - Node getEnumerateTerm( TypeNode tn, unsigned index ); - + Node getEnumerateTerm( TypeNode tn, unsigned index ); + //miscellaneous public: /** map from universal quantifiers to the list of variables */ @@ -353,7 +354,7 @@ public: int getQAttrQuantInstLevel( Node q ); /** get rewrite rule priority */ int getQAttrRewriteRulePriority( Node q ); - + };/* class TermDb */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 12edaa31c..951a6b545 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -131,6 +131,9 @@ void TheoryQuantifiers::check(Effort e) { break; case kind::INST_CLOSURE: getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true ); + if( !options::lteRestrictInstClosure() ){ + getQuantifiersEngine()->getMasterEqualityEngine()->addTerm( assertion[0] ); + } break; case kind::EQUAL: //do nothing diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 52b4fd17d..13822eb98 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -80,9 +80,9 @@ d_lemmas_produced_c(u){ //d_rr_tr_trie = new rrinst::TriggerTrie; //d_eem = new EfficientEMatcher( this ); d_hasAddedLemma = false; - + bool needsBuilder = false; - + Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; //the model object @@ -158,7 +158,7 @@ d_lemmas_produced_c(u){ }else{ d_lte_part_inst = NULL; } - + if( needsBuilder ){ Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || @@ -604,21 +604,35 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){ } bool QuantifiersEngine::isTermEligibleForInstantiation( Node n, Node f, bool print ) { - if( n.hasAttribute(InstLevelAttribute()) ){ - int fml = d_term_db->getQAttrQuantInstLevel( f ); - unsigned ml = fml>=0 ? fml : options::instMaxLevel(); - - if( n.getAttribute(InstLevelAttribute())>ml ){ - Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute()); - Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl; + if( options::lteRestrictInstClosure() ){ + //has to be both in inst closure and in ground assertions + if( !d_term_db->isInstClosure( n ) ){ + Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl; return false; } - }else{ - if( options::instLevelInputOnly() ){ - Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl; + // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this + if( !d_term_db->hasTermCurrent( n, false ) ){ + Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl; return false; } } + if( options::instMaxLevel()!=-1 ){ + if( n.hasAttribute(InstLevelAttribute()) ){ + int fml = d_term_db->getQAttrQuantInstLevel( f ); + unsigned ml = fml>=0 ? fml : options::instMaxLevel(); + + if( n.getAttribute(InstLevelAttribute())>ml ){ + Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute()); + Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl; + return false; + } + }else{ + if( options::instLevelInputOnly() ){ + Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl; + return false; + } + } + } return true; } @@ -775,7 +789,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo Trace("inst-add-debug") << std::endl; //check based on instantiation level - if( options::instMaxLevel()!=-1 ){ + if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ for( unsigned i=0; igetTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){ + return -1; + }else if( options::instMaxLevel()!=-1 ){ //score prefer lowest instantiation level if( n.hasAttribute(InstLevelAttribute()) ){ s = n.getAttribute(InstLevelAttribute()); -- 2.30.2