From: Andrew Reynolds Date: Thu, 8 May 2014 13:13:05 +0000 (-0500) Subject: Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Minor fixes... X-Git-Tag: cvc5-1.0.0~6920 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ce831651caf58c1005fd3ebfdd2b75923d594328;p=cvc5.git Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Minor fixes to ambqi. Preparation for CASC proof output. Add NNF option. --- diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index e3f031d11..7f119ae93 100755 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -863,7 +863,7 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) { Assert( n.getKind()!=FORALL ); - if( n.getKind()==NOT ){ + if( n.getKind()==NOT && n[0].getKind()!=FORALL ){ doCheck( m, q, ad, n[0] ); ad.negate(); return true; diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index a74c51a9a..096d0cab2 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -198,6 +198,24 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No } } +void InstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const { + if( terms.size()==q[0].getNumChildren() ){ + Trace(c) << " ( "; + for( unsigned i=0; i0 ) Trace(c) << ", "; + Trace(c) << terms[i]; + } + Trace(c) << " )" << std::endl; + }else{ + for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ + terms.push_back( it->first ); + it->second.print( c, q, terms ); + terms.pop_back(); + } + } +} + + bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){ bool reset = false; @@ -264,6 +282,25 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< } } +void CDInstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const{ + if( d_valid.get() ){ + if( terms.size()==q[0].getNumChildren() ){ + Trace(c) << " ( "; + for( unsigned i=0; i0 ) Trace(c) << ", "; + Trace(c) << terms[i]; + } + Trace(c) << " )" << std::endl; + }else{ + for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ + terms.push_back( it->first ); + it->second->print( c, q, terms ); + terms.pop_back(); + } + } + } +} + }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index c366c4a09..2cf63210b 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -100,6 +100,8 @@ public: public: /** the data */ std::map< Node, InstMatchTrie > d_data; +private: + void print( const char * c, Node q, std::vector< Node >& terms ) const; public: InstMatchTrie(){} ~InstMatchTrie(){} @@ -126,6 +128,10 @@ public: } bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); + void print( const char * c, Node q ) const{ + std::vector< Node > terms; + print( c, q, terms ); + } };/* class InstMatchTrie */ /** trie for InstMatch objects */ @@ -135,6 +141,8 @@ public: std::map< Node, CDInstMatchTrie* > d_data; /** is valid */ context::CDO< bool > d_valid; +private: + void print( const char * c, Node q, std::vector< Node >& terms ) const; public: CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} ~CDInstMatchTrie(){} @@ -161,6 +169,10 @@ public: } bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0, bool onlyExist = false ); + void print( const char * c, Node q ) const{ + std::vector< Node > terms; + print( c, q, terms ); + } };/* class CDInstMatchTrie */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 10c538dd9..38db10feb 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -33,6 +33,9 @@ option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true # Whether to CNF quantifier bodies option cnfQuant --cnf-quant bool :default false apply CNF conversion to quantified formulas +# Whether to NNF quantifier bodies +option nnfQuant --nnf-quant bool :default false + apply NNF conversion to quantified formulas option clauseSplit --clause-split bool :default false apply clause splitting to quantified formulas diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 38fc1d919..c42c16043 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -139,7 +139,7 @@ void QuantifiersRewriter::setNestedQuantifiers2( Node n, Node q, std::vector< No if( n.getKind()==FORALL || n.getKind()==EXISTS ){ Trace("quantifiers-rewrite-debug") << "Set nested quant attribute " << n << std::endl; NestedQuantAttribute nqai; - n.setAttribute(nqai,q); + n[0].setAttribute(nqai,q); } for( int i=0; i<(int)n.getNumChildren(); i++ ){ setNestedQuantifiers2( n[i], q, processed ); @@ -148,8 +148,8 @@ void QuantifiersRewriter::setNestedQuantifiers2( Node n, Node q, std::vector< No } RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { - Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl; if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){ + Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in[0].hasAttribute(NestedQuantAttribute()) << std::endl; if( !in.hasAttribute(NestedQuantAttribute()) ){ setNestedQuantifiers( in[ 1 ], in ); } @@ -188,7 +188,7 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl; - Trace("quantifiers-rewrite-debug") << "Attributes : " << in.hasAttribute(NestedQuantAttribute()) << std::endl; + Trace("quantifiers-rewrite-debug") << "Attributes : " << in[0].hasAttribute(NestedQuantAttribute()) << std::endl; if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){ RewriteStatus status = REWRITE_DONE; Node ret = in; @@ -214,10 +214,10 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { ret = ret.negate(); status = REWRITE_AGAIN_FULL; }else{ - bool isNested = in.hasAttribute(NestedQuantAttribute()); + bool isNested = in[0].hasAttribute(NestedQuantAttribute()); for( int op=0; op& args, NodeBuilder<>& defs, bool forcePred ){ @@ -691,68 +688,6 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& return f; } -//general method for computing various rewrites -Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){ - if( f.getKind()==FORALL ){ - Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << std::endl; - std::vector< Node > args; - for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ - args.push_back( f[0][i] ); - } - NodeBuilder<> defs(kind::AND); - Node n = f[1]; - Node ipl; - if( f.getNumChildren()==3 ){ - ipl = f[2]; - } - if( computeOption==COMPUTE_ELIM_SYMBOLS ){ - n = computeElimSymbols( n ); - }else if( computeOption==COMPUTE_MINISCOPING ){ - //return directly - return computeMiniscoping( f, args, n, ipl, f.hasAttribute(NestedQuantAttribute()) ); - }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ - return computeAggressiveMiniscoping( args, n, f.hasAttribute(NestedQuantAttribute()) ); - }else if( computeOption==COMPUTE_NNF ){ - n = computeNNF( n ); - }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){ - n = computeSimpleIteLift( n ); - }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() ); - }else if( computeOption==COMPUTE_CNF ){ - //n = computeNNF( n ); - n = computeCNF( n, args, defs, false ); - ipl = Node::null(); - }else if( computeOption==COMPUTE_SPLIT ) { - return computeSplit(f, n, args ); - } - Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl; - if( f[1]==n && args.size()==f[0].getNumChildren() ){ - return f; - }else{ - if( args.empty() ){ - defs << n; - }else{ - std::vector< Node > children; - children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); - children.push_back( n ); - if( !ipl.isNull() ){ - children.push_back( ipl ); - } - defs << NodeManager::currentNM()->mkNode(kind::FORALL, children ); - } - return defs.getNumChildren()==1 ? defs.getChild( 0 ) : defs.constructNode(); - } - }else{ - return f; - } -} - Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){ std::vector< Node > activeArgs; computeArgVec( args, activeArgs, body ); @@ -973,15 +908,15 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ return options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_NNF ){ - return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities) + return options::nnfQuant(); }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){ - return options::simpleIteLiftQuant();//!options::finiteModelFind(); + return options::simpleIteLiftQuant(); }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant() && !options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return options::varElimQuant(); }else if( computeOption==COMPUTE_CNF ){ - return false;//return options::cnfQuant() ; + return false;//return options::cnfQuant() ; FIXME }else if( computeOption==COMPUTE_SPLIT ){ return options::clauseSplit(); }else{ @@ -989,7 +924,67 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption } } - +//general method for computing various rewrites +Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOption ){ + if( f.getKind()==FORALL ){ + Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << ", nested = " << isNested << std::endl; + std::vector< Node > args; + for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ + args.push_back( f[0][i] ); + } + NodeBuilder<> defs(kind::AND); + Node n = f[1]; + Node ipl; + if( f.getNumChildren()==3 ){ + ipl = f[2]; + } + if( computeOption==COMPUTE_ELIM_SYMBOLS ){ + n = computeElimSymbols( n ); + }else if( computeOption==COMPUTE_MINISCOPING ){ + //return directly + return computeMiniscoping( f, args, n, ipl, isNested ); + }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ + return computeAggressiveMiniscoping( args, n, isNested ); + }else if( computeOption==COMPUTE_NNF ){ + n = computeNNF( n ); + }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){ + n = computeSimpleIteLift( n ); + }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() ); + }else if( computeOption==COMPUTE_CNF ){ + //n = computeNNF( n ); + n = computeCNF( n, args, defs, false ); + ipl = Node::null(); + }else if( computeOption==COMPUTE_SPLIT ) { + return computeSplit(f, n, args ); + } + Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl; + if( f[1]==n && args.size()==f[0].getNumChildren() ){ + return f; + }else{ + if( args.empty() ){ + defs << n; + }else{ + std::vector< Node > children; + children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); + children.push_back( n ); + if( !ipl.isNull() ){ + children.push_back( ipl ); + } + defs << NodeManager::currentNM()->mkNode(kind::FORALL, children ); + } + return defs.getNumChildren()==1 ? defs.getChild( 0 ) : defs.constructNode(); + } + }else{ + return f; + } +} Node QuantifiersRewriter::rewriteRewriteRule( Node r ) { diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 0cb76f686..a6a8a6780 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -69,7 +69,7 @@ private: COMPUTE_SPLIT, COMPUTE_LAST }; - static Node computeOperation( Node f, int computeOption ); + static Node computeOperation( Node f, bool isNested, int computeOption ); public: static RewriteResponse preRewrite(TNode in); static RewriteResponse postRewrite(TNode in); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 964ea9c73..64965f5ce 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -506,7 +506,7 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes } } } - + Trace("quantifiers-sk") << "mkSkolem body for " << f << " returns : " << ret << std::endl; return ret; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 929a638d7..8fecc6ee0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -623,6 +623,20 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ } } +void QuantifiersEngine::printInstantiations( const char * c ) { + if( options::incrementalSolving() ){ + for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ + Trace(c) << "Instantiations of " << it->first << " : " << std::endl; + it->second->print( c, it->first ); + } + }else{ + for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ + Trace(c) << "Instantiations of " << it->first << " : " << std::endl; + it->second.print( c, it->first ); + } + } +} + QuantifiersEngine::Statistics::Statistics(): d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index eb9803592..7a899db0c 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -235,6 +235,8 @@ public: /** get the master equality engine */ eq::EqualityEngine* getMasterEqualityEngine() ; public: + /** print instantiations */ + void printInstantiations( const char * c ); /** statistics class */ class Statistics { public: