From 63c1d547b7598e3dba35f865ba3749c15a105a6f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 11 Mar 2013 16:29:22 -0500 Subject: [PATCH] ite removal option for quantifiers --ite-remove-quant, e-matching for boolean terms, improvement for pre skolemization --- src/smt/smt_engine.cpp | 79 ++++++++++--------- src/theory/quantifiers/inst_match.cpp | 2 +- .../quantifiers/inst_match_generator.cpp | 22 ++++-- .../quantifiers/inst_strategy_e_matching.cpp | 7 ++ src/theory/quantifiers/options | 5 +- src/theory/quantifiers/quant_util.h | 2 + src/theory/quantifiers/trigger.cpp | 35 ++++++-- src/theory/quantifiers/trigger.h | 3 +- src/theory/quantifiers_engine.cpp | 12 ++- src/theory/quantifiers_engine.h | 6 +- src/util/ite_removal.cpp | 45 +++++++++-- src/util/ite_removal.h | 2 +- 12 files changed, 152 insertions(+), 68 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8eb6664ca..e7b3daa2b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1427,17 +1427,27 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map ContainsQuantAttribute; + // check if the given node contains a universal quantifier static bool containsQuantifiers(Node n) { - if(n.getKind() == kind::FORALL) { + if( n.hasAttribute(ContainsQuantAttribute()) ){ + return n.getAttribute(ContainsQuantAttribute())==1; + } else if(n.getKind() == kind::FORALL) { return true; } else { - for(unsigned i = 0; i < n.getNumChildren(); ++i) { - if(containsQuantifiers(n[i])) { - return true; + bool cq = false; + for( unsigned i = 0; i < n.getNumChildren(); ++i ){ + if( containsQuantifiers(n[i]) ){ + cq = true; + break; } } - return false; + ContainsQuantAttribute cqa; + n.setAttribute(cqa, cq ? 1 : 0); + return cq; } } @@ -1498,43 +1508,36 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect } }else{ //check if it contains a quantifier as a subterm - bool containsQuant = false; - if( n.getType().isBoolean() ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( containsQuantifiers( n[i] ) ){ - containsQuant = true; - break; - } - } - } //if so, we will write this node - if( containsQuant ){ - if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){ - Node nn; - //must remove structure - if( n.getKind()==kind::ITE ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); - }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); - }else if( n.getKind()==kind::IMPLIES ){ - nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); - } - return preSkolemizeQuantifiers( nn, polarity, fvs ); - }else{ - Assert( n.getKind() == kind::AND || n.getKind() == kind::OR ); - vector< Node > children; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) ); + if( containsQuantifiers( n ) ){ + if( n.getType().isBoolean() ){ + if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){ + Node nn; + //must remove structure + if( n.getKind()==kind::ITE ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); + }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); + }else if( n.getKind()==kind::IMPLIES ){ + nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); + } + return preSkolemizeQuantifiers( nn, polarity, fvs ); + }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){ + vector< Node > children; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + //must pull ite's } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); } - }else{ - return n; } + return n; } } diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 85a96f90a..5a80512cd 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -140,7 +140,7 @@ void InstMatch::set(TNode var, TNode n){ //var.getType() == n.getType() !n.getType().isSubtypeOf( var.getType() ) ){ Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl; - Trace("inst-match-warn") << var << " " << var.getType() << n << " " << n.getType() << std::endl ; + Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ; Assert(false); } d_map[var] = n; diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 5484e25e9..dd8588b52 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -74,7 +74,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat int childMatchPolicy = MATCH_GEN_DEFAULT; for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){ - if( d_match_pattern[i].getKind()!=INST_CONSTANT ){ + if( d_match_pattern[i].getKind()!=INST_CONSTANT && !Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ InstMatchGenerator * cimg = new InstMatchGenerator( d_match_pattern[i], childMatchPolicy ); d_children.push_back( cimg ); d_children_index.push_back( i ); @@ -115,7 +115,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); }else{ d_cg = new CandidateGeneratorQueue; - if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){ + if( !Trigger::isArithmeticTrigger( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){ Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; @@ -155,14 +155,20 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi //first, check if ground arguments are not equal, or a match is in conflict for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){ - if( d_match_pattern[i].getKind()==INST_CONSTANT ){ - if( !m.setMatch( q, d_match_pattern[i], t[i] ) ){ + if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ + Node vv = d_match_pattern[i]; + Node tt = t[i]; + if( Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ + vv = d_match_pattern[i][0]; + tt = NodeManager::currentNM()->mkConst(q->areEqual( tt, d_match_pattern[i][1] )); + } + if( !m.setMatch( q, vv, tt ) ){ //match is in conflict - Debug("matching-debug") << "Match in conflict " << t[i] << " and " - << d_match_pattern[i] << " because " - << m.get(d_match_pattern[i]) + Debug("matching-debug") << "Match in conflict " << tt << " and " + << vv << " because " + << m.get(vv) << std::endl; - Debug("matching-fail") << "Match fail: " << m.get(d_match_pattern[i]) << " and " << t[i] << std::endl; + Debug("matching-fail") << "Match fail: " << m.get(vv) << " and " << tt << std::endl; success = false; break; } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 3f5cc7666..0915f59a5 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -145,6 +145,10 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) if( gen ){ generateTriggers( f, effort, e, status ); } + //if( e==4 ){ + // d_processed_trigger.clear(); + // d_quantEngine->getEqualityQuery()->setLiberal( true ); + //} Debug("quant-uf-strategy") << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl; //Notice() << "Try auto-generated triggers..." << std::endl; for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){ @@ -171,6 +175,9 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) } } } + //if( e==4 ){ + // d_quantEngine->getEqualityQuery()->setLiberal( false ); + //} Debug("quant-uf-strategy") << "done." << std::endl; //Notice() << "done" << std::endl; return status; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 7a3687dd5..222fc4425 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -36,7 +36,8 @@ option cnfQuant --cnf-quant bool :default false # forall x. P( x ) => f( S( x ) ) = x option preSkolemQuant --pre-skolem-quant bool :default false apply skolemization eagerly to bodies of quantified formulas - +option iteRemoveQuant --ite-remove-quant bool :default false + apply ite removal to bodies of quantifiers # Whether to perform agressive miniscoping option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false perform aggressive miniscoping for quantifiers @@ -48,7 +49,7 @@ option macrosQuant --macros-quant bool :default false option smartTriggers /--disable-smart-triggers bool :default true disable smart triggers # Whether to use relevent triggers -option relevantTriggers --relevant-triggers bool :default true +option relevantTriggers /--disable-relevant-triggers bool :default true prefer triggers that are more relevant based on SInE style analysis # Whether to consider terms in the bodies of quantifiers for matching diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 85602dbab..0b4f2654b 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -91,6 +91,8 @@ public: virtual eq::EqualityEngine* getEngine() = 0; /** get the equivalence class of a */ virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0; + + virtual void setLiberal( bool l ) = 0; };/* class EqualityQuery */ } diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index cff28f243..125829e06 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -226,17 +226,24 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ bool Trigger::isUsable( Node n, Node f ){ if( n.getAttribute(InstConstantAttribute())==f ){ - if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){ - std::map< Node, Node > coeffs; - return getPatternArithmetic( f, n, coeffs ); - }else{ + if( isAtomicTrigger( n ) ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ if( !isUsable( n[i], f ) ){ return false; } } return true; + }else if( n.getKind()==INST_CONSTANT ){ + return true; + }else{ + std::map< Node, Node > coeffs; + if( isArithmeticTrigger( f, n, coeffs ) ){ + return true; + }else if( isBooleanTermTrigger( n ) ){ + return true; + } } + return false; }else{ return true; } @@ -368,7 +375,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } -bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){ +bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs ){ if( n.getKind()==PLUS ){ Assert( coeffs.empty() ); NodeBuilder<> t(kind::PLUS); @@ -381,7 +388,7 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef coeffs.clear(); return false; } - }else if( !getPatternArithmetic( f, n[i], coeffs ) ){ + }else if( !isArithmeticTrigger( f, n[i], coeffs ) ){ coeffs.clear(); return false; } @@ -413,6 +420,22 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef return false; } +bool Trigger::isBooleanTermTrigger( Node n ) { + if( n.getKind()==ITE ){ + //check for boolean term converted to ITE + if( n[0].getKind()==INST_CONSTANT && + n[1].getKind()==CONST_BITVECTOR && + n[2].getKind()==CONST_BITVECTOR ){ + if( ((BitVectorType)n[1].getType().toType()).getSize()==1 && + n[1].getConst().toInteger()==1 && + n[2].getConst().toInteger()==0 ){ + return true; + } + } + } + return false; +} + Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){ if( nodes.empty() ){ return d_tr; diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 93731283b..9ecac0120 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -109,7 +109,8 @@ public: static bool isAtomicTrigger( Node n ); static bool isSimpleTrigger( Node n ); /** get pattern arithmetic */ - static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ); + static bool isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs ); + static bool isBooleanTermTrigger( Node n ); inline void toStream(std::ostream& out) const { out << "TRIGGER( "; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a11cc85c0..f12143bbe 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -583,12 +583,16 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ return true; }else{ eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - if( ee->areEqual( a, b ) ){ - return true; + if( d_liberal ){ + return true;//!areDisequal( a, b ); + }else{ + if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ + if( ee->areEqual( a, b ) ){ + return true; + } } + return false; } - return false; } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 9f520f420..5f288a186 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -272,6 +272,8 @@ private: std::map< Node, int > d_rep_score; /** reset count */ int d_reset_count; + + bool d_liberal; private: /** node contains */ Node getInstance( Node n, std::vector< Node >& eqc ); @@ -280,7 +282,7 @@ private: /** choose rep based on sort inference */ bool optInternalRepSortInference(); public: - EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){} + EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){} ~EqualityQueryQuantifiersEngine(){} /** reset */ void reset(); @@ -296,6 +298,8 @@ public: not contain instantiation constants, if such a term exists. */ Node getInternalRepresentative( Node a, Node f, int index ); + + void setLiberal( bool l ) { d_liberal = l; } }; /* EqualityQueryQuantifiersEngine */ }/* CVC4::theory namespace */ diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index 240e5a0cf..de7ae2e97 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -19,6 +19,7 @@ #include "util/ite_removal.h" #include "theory/rewriter.h" #include "expr/command.h" +#include "theory/quantifiers/options.h" using namespace CVC4; using namespace std; @@ -28,12 +29,13 @@ namespace CVC4 { void RemoveITE::run(std::vector& output, IteSkolemMap& iteSkolemMap) { for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { - output[i] = run(output[i], output, iteSkolemMap); + std::vector quantVar; + output[i] = run(output[i], output, iteSkolemMap, quantVar); } } Node RemoveITE::run(TNode node, std::vector& output, - IteSkolemMap& iteSkolemMap) { + IteSkolemMap& iteSkolemMap, std::vector& quantVar) { // Current node Debug("ite") << "removeITEs(" << node << ")" << endl; @@ -50,8 +52,23 @@ Node RemoveITE::run(TNode node, std::vector& output, if(node.getKind() == kind::ITE) { TypeNode nodeType = node.getType(); if(!nodeType.isBoolean()) { + Node skolem; // Make the skolem to represent the ITE - Node skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal"); + if( quantVar.empty() ){ + skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal"); + }else{ + //if in the scope of free variables, make a skolem operator + vector< TypeNode > argTypes; + for( size_t i=0; imkFunctionType( argTypes, nodeType ); + Node op = NodeManager::currentNM()->mkSkolem( "termITEop_$$", typ, "a function variable introduced due to term-level ITE removal" ); + vector< Node > funcArgs; + funcArgs.push_back( op ); + funcArgs.insert( funcArgs.end(), quantVar.begin(), quantVar.end() ); + skolem = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ); + } // The new assertion Node newAssertion = @@ -63,7 +80,16 @@ Node RemoveITE::run(TNode node, std::vector& output, d_iteCache[node] = skolem; // Remove ITEs from the new assertion, rewrite it and push it to the output - newAssertion = run(newAssertion, output, iteSkolemMap); + newAssertion = run(newAssertion, output, iteSkolemMap, quantVar); + + if( !quantVar.empty() ){ + //if in the scope of free variables, it is a quantified assertion + vector< Node > children; + children.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, quantVar ) ); + children.push_back( newAssertion ); + newAssertion = NodeManager::currentNM()->mkNode( kind::FORALL, children ); + } + iteSkolemMap[skolem] = output.size(); output.push_back(newAssertion); @@ -73,9 +99,16 @@ Node RemoveITE::run(TNode node, std::vector& output, } // If not an ITE, go deep - if( node.getKind() != kind::FORALL && + if( ( node.getKind() != kind::FORALL || options::iteRemoveQuant() ) && node.getKind() != kind::EXISTS && node.getKind() != kind::REWRITE_RULE ) { + std::vector< Node > newQuantVar; + newQuantVar.insert( newQuantVar.end(), quantVar.begin(), quantVar.end() ); + if( node.getKind()==kind::FORALL ){ + for( size_t i=0; i newChildren; bool somethingChanged = false; if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { @@ -83,7 +116,7 @@ Node RemoveITE::run(TNode node, std::vector& output, } // Remove the ITEs from the children for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = run(*it, output, iteSkolemMap); + Node newChild = run(*it, output, iteSkolemMap, newQuantVar); somethingChanged |= (newChild != *it); newChildren.push_back(newChild); } diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h index 77e9c39db..6c0c74cd4 100644 --- a/src/util/ite_removal.h +++ b/src/util/ite_removal.h @@ -55,7 +55,7 @@ public: * ite created in conjunction with that skolem variable. */ Node run(TNode node, std::vector& additionalAssertions, - IteSkolemMap& iteSkolemMap); + IteSkolemMap& iteSkolemMap, std::vector& quantVar); };/* class RemoveTTE */ -- 2.30.2