From: ajreynol Date: Wed, 1 Jul 2015 16:42:43 +0000 (+0200) Subject: Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-quant... X-Git-Tag: cvc5-1.0.0~6267^2~7 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d475d255f3c61380524517cd9b97725dcb0c9c22;p=cvc5.git Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-quant. Minor bug fixes for internalReps, alpha equivalence. Update casc 25 FOF script. --- diff --git a/contrib/run-script-casc25-fof b/contrib/run-script-casc25-fof index b6bea37dd..7717abe47 100755 --- a/contrib/run-script-casc25-fof +++ b/contrib/run-script-casc25-fof @@ -15,7 +15,7 @@ echo "------- cvc4-fof casc 25 : $bench at $2..." function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null | + (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump --quant-alpha-equiv "$@" $bench) 2>/dev/null | (read w1 w2 w3 result w4 w5; case "$result" in Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; @@ -25,13 +25,13 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench + $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump --quant-alpha-equiv "$@" $bench } # designed for 300 seconds trywith 15 --relevant-triggers --clause-split --full-saturate-quant trywith 15 --clause-split --no-e-matching --full-saturate-quant -trywith 15 --finite-model-find --quant-cf --sort-inference --uf-ss-fair +trywith 15 --finite-model-find --quant-cf --qcf-all-conflict --sort-inference --uf-ss-fair trywith 5 --trigger-sel=max --full-saturate-quant trywith 5 --relevant-triggers --clause-split --multi-trigger-when-single --full-saturate-quant trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant @@ -39,7 +39,7 @@ trywith 5 --pre-skolem-quant --no-pre-skolem-quant-nested --full-saturate-quant trywith 15 --relevant-triggers --decision=internal --full-saturate-quant trywith 15 --clause-split --no-quant-cf --full-saturate-quant trywith 15 --clause-split --trigger-sel=min --full-saturate-quant -trywith 30 --relevant-triggers --prenex-quant=none --full-saturate-quant +trywith 30 --prenex-quant=none --full-saturate-quant trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev finishwith --term-db-mode=relevant --full-saturate-quant diff --git a/contrib/run-script-casc25-tfa b/contrib/run-script-casc25-tfa new file mode 100644 index 000000000..463b5396e --- /dev/null +++ b/contrib/run-script-casc25-tfa @@ -0,0 +1,40 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-tfa casc 25 : $bench at $2..." + +# use: trywith [params..] +# to attempt a run. If an SZS ontology result is printed, then +# the run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + limit=$1; shift; + echo "--- Run $@ at $limit..."; + (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null | + (read w1 w2 w3 result w4 w5; + case "$result" in + Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} +function finishwith { + echo "--- Run $@..."; + $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench +} + +trywith 10 --cbqi2 --decision=internal --full-saturate-quant +trywith 10 --relevant-triggers --full-saturate-quant +trywith 10 --cbqi --full-saturate-quant +trywith 30 --qcf-tconstraint --full-saturate-quant +trywith 60 --cbqi --cbqi-recurse --full-saturate-quant +trywith 10 --full-saturate-quant +trywith 10 --no-e-matching --full-saturate-quant +trywith 10 --fmf-bound-int +finishwith --cbqi2 --cbqi-recurse --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-casc25-tff b/contrib/run-script-casc25-tff deleted file mode 100644 index 9313b7886..000000000 --- a/contrib/run-script-casc25-tff +++ /dev/null @@ -1,40 +0,0 @@ -#!/bin/bash - -cvc4=./cvc4 -bench="$1" - -file=${bench##*/} -filename=${file%.*} - -echo "------- cvc4-tff casc 25 : $bench at $2..." - -# use: trywith [params..] -# to attempt a run. If an SZS ontology result is printed, then -# the run script terminates immediately. Otherwise, this -# function returns normally. -function trywith { - limit=$1; shift; - echo "--- Run $@ at $limit..."; - (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null | - (read w1 w2 w3 result w4 w5; - case "$result" in - Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; - Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; - esac; exit 1) - if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi -} -function finishwith { - echo "--- Run $@..."; - $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench -} - -trywith 10 --cbqi2 --decision=internal --full-saturate-quant -trywith 10 --relevant-triggers --full-saturate-quant -trywith 10 --cbqi --full-saturate-quant -trywith 30 --qcf-tconstraint --full-saturate-quant -trywith 60 --cbqi --cbqi-recurse --full-saturate-quant -trywith 10 --full-saturate-quant -trywith 10 --no-e-matching --full-saturate-quant -trywith 10 --fmf-bound-int -finishwith --cbqi2 --cbqi-recurse --full-saturate-quant -# echo "% SZS status" "GaveUp for $filename" diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 47cb62715..97ad3e8ea 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -143,6 +143,14 @@ typedef enum { TERM_DB_RELEVANT, } TermDbMode; +typedef enum { + /** do not lift ITEs in quantified formulas */ + ITE_LIFT_QUANT_MODE_NONE, + /** only lift ITEs in quantified formulas if reduces the term size */ + ITE_LIFT_QUANT_MODE_SIMPLE, + /** lift ITEs */ + ITE_LIFT_QUANT_MODE_ALL, +} IteLiftQuantMode; }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index e34465d9b..231392a9a 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -19,7 +19,7 @@ option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write disable miniscope quantifiers for ground subformulas # Whether to prenex (nested universal) quantifiers option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h" - disable prenexing of quantified formulas + prenex mode for quantified formulas # Whether to variable-eliminate quantifiers. # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to # forall y. P( c, y ) @@ -27,13 +27,16 @@ option varElimQuant --var-elim-quant bool :default true disable simple variable elimination for quantified formulas option dtVarExpandQuant --dt-var-exp-quant bool :default true expand datatype variables bound to one constructor in quantifiers +#ite lift mode for quantified formulas +option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToIteLiftQuantMode :handler-include "theory/quantifiers/options_handlers.h" + ite lifting mode for quantified formulas option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true split variables occurring as conditions of ITE in quantifiers -option simpleIteLiftQuant --ite-lift-quant bool :default true - disable simple ite lifting for quantified formulas +option iteDtTesterSplitQuant --ite-dtt-split-quant bool :default false + split ites with dt testers as conditions # Whether to CNF quantifier bodies -option cnfQuant --cnf-quant bool :default false - apply CNF conversion to quantified formulas +# option cnfQuant --cnf-quant bool :default false +# apply CNF conversion to quantified formulas # Whether to NNF quantifier bodies option nnfQuant --nnf-quant bool :default true apply NNF conversion to quantified formulas @@ -159,6 +162,8 @@ option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode : when to invoke conflict find mechanism for quantifiers option qcfTConstraint --qcf-tconstraint bool :read-write :default false enable entailment checks for t-constraints in qcf algorithm +option qcfAllConflict --qcf-all-conflict bool :read-write :default false + add all available conflicting instances during conflict-based instantiation option instNoEntail --inst-no-entail bool :read-write :default true do not consider instances of quantified formulas that are currently entailed @@ -191,7 +196,7 @@ option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write filter based on canonicity option conjectureFilterModel --conjecture-filter-model bool :read-write :default true filter based on model -option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0 +option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50 number of ground terms to generate for model filtering option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false more aggressive merging for universal equality engine, introduces terms diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 9fb5dd69d..c518813a0 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -204,6 +204,19 @@ relevant \n\ + Quantifiers module considers only ground terms connected to current assertions. \n\ \n\ "; +static const std::string iteLiftQuantHelp = "\ +Modes for term database, supported by --ite-lift-quant:\n\ +\n\ +all \n\ ++ Do not lift if-then-else in quantified formulas.\n\ +\n\ +simple \n\ ++ Lift if-then-else in quantified formulas if results in smaller term size.\n\ +\n\ +none \n\ ++ Lift if-then-else in quantified formulas. \n\ +\n\ +"; inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { @@ -414,6 +427,22 @@ inline TermDbMode stringToTermDbMode(std::string option, std::string optarg, Smt } } +inline IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "all" ) { + return ITE_LIFT_QUANT_MODE_ALL; + } else if(optarg == "simple") { + return ITE_LIFT_QUANT_MODE_SIMPLE; + } else if(optarg == "none") { + return ITE_LIFT_QUANT_MODE_NONE; + } else if(optarg == "help") { + puts(iteLiftQuantHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --ite-lift-quant: `") + + optarg + "'. Try --ite-lift-quant help."); + } +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 18bffe908..47c2e1c5b 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1971,6 +1971,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { Trace("qcf-debug") << std::endl; } short end_e = getMaxQcfEffort(); + bool isConflict = false; for( short e = effort_conflict; e<=end_e; e++ ){ d_effort = e; Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl; @@ -2014,8 +2015,12 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { ++addedLemmas; if( e==effort_conflict ){ d_quant_order.insert( d_quant_order.begin(), q ); - d_conflict.set( true ); ++(d_statistics.d_conflict_inst); + if( options::qcfAllConflict() ){ + isConflict = true; + }else{ + d_conflict.set( true ); + } break; }else if( e==effort_prop_eq ){ ++(d_statistics.d_prop_inst); @@ -2044,6 +2049,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { break; } } + if( isConflict ){ + d_conflict.set( true ); + } if( Trace.isOn("qcf-engine") ){ double clSet2 = double(clock())/double(CLOCKS_PER_SEC); Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0afdece82..07aa89ece 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -340,64 +340,141 @@ Node QuantifiersRewriter::computeNNF( Node body ){ } } + +void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, + std::vector< Node >& conj ){ + if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){ + Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl; + Node x = n[0][0]; + std::map< Node, Node >::iterator itp = pcons.find( x ); + if( itp!=pcons.end() ){ + Trace("quantifiers-rewrite-ite-debug") << "...condition already set " << itp->second << std::endl; + computeDtTesterIteSplit( n[ itp->second==n[0] ? 1 : 2 ], pcons, ncons, conj ); + }else{ + Expr testerExpr = n[0].getOperator().toExpr(); + int index = Datatype::indexOf( testerExpr ); + std::map< int, Node >::iterator itn = ncons[x].find( index ); + if( itn!=ncons[x].end() ){ + Trace("quantifiers-rewrite-ite-debug") << "...condition negated " << itn->second << std::endl; + computeDtTesterIteSplit( n[ 2 ], pcons, ncons, conj ); + }else{ + for( unsigned i=0; i<2; i++ ){ + if( i==0 ){ + pcons[x] = n[0]; + }else{ + pcons.erase( x ); + ncons[x][index] = n[0].negate(); + } + computeDtTesterIteSplit( n[i+1], pcons, ncons, conj ); + } + ncons[x].erase( index ); + } + } + }else{ + Trace("quantifiers-rewrite-ite-debug") << "Return value : " << n << std::endl; + std::vector< Node > children; + children.push_back( n ); + std::vector< Node > vars; + //add all positive testers + for( std::map< Node, Node >::iterator it = pcons.begin(); it != pcons.end(); ++it ){ + children.push_back( it->second.negate() ); + vars.push_back( it->first ); + } + //add all negative testers + for( std::map< Node, std::map< int, Node > >::iterator it = ncons.begin(); it != ncons.end(); ++it ){ + Node x = it->first; + //only if we haven't settled on a positive tester + if( std::find( vars.begin(), vars.end(), x )==vars.end() ){ + //check if we have exhausted all options but one + const Datatype& dt = DatatypeType(x.getType().toType()).getDatatype(); + std::vector< Node > nchildren; + int pos_cons = -1; + for( int i=0; i<(int)dt.getNumConstructors(); i++ ){ + std::map< int, Node >::iterator itt = it->second.find( i ); + if( itt==it->second.end() ){ + pos_cons = pos_cons==-1 ? i : -2; + }else{ + nchildren.push_back( itt->second.negate() ); + } + } + if( pos_cons>=0 ){ + const DatatypeConstructor& c = dt[pos_cons]; + Expr tester = c.getTester(); + children.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), x ).negate() ); + }else{ + children.insert( children.end(), nchildren.begin(), nchildren.end() ); + } + } + } + //make condition/output pair + Node c = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + conj.push_back( c ); + } +} + Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) { if( body.getType().isBoolean() ){ - if( body.getKind()==EQUAL && options::simpleIteLiftQuant() ){ + if( body.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){ for( size_t i=0; i<2; i++ ){ if( body[i].getKind()==ITE ){ Node no = i==0 ? body[1] : body[0]; - bool doRewrite = false; - std::vector< Node > children; - children.push_back( body[i][0] ); - for( size_t j=1; j<=2; j++ ){ - //check if it rewrites to a constant - Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] ); - nn = Rewriter::rewrite( nn ); - children.push_back( nn ); - if( nn.isConst() ){ - doRewrite = true; + if( no.getKind()!=ITE ){ + bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL; + std::vector< Node > children; + children.push_back( body[i][0] ); + for( size_t j=1; j<=2; j++ ){ + //check if it rewrites to a constant + Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] ); + nn = Rewriter::rewrite( nn ); + children.push_back( nn ); + if( nn.isConst() ){ + doRewrite = true; + } + } + if( doRewrite ){ + return NodeManager::currentNM()->mkNode( ITE, children ); } - } - if( doRewrite ){ - return NodeManager::currentNM()->mkNode( ITE, children ); } } } - }else if( body.getKind()==ITE && hasPol && options::iteCondVarSplitQuant() ){ - for( unsigned r=0; r<2; r++ ){ - //check if there is a variable elimination - Node b = r==0 ? body[0] : body[0].negate(); - QuantPhaseReq qpr( b ); - std::vector< Node > vars; - std::vector< Node > subs; - Trace("ite-var-split-quant") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl; - for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ - Trace("ite-var-split-quant") << "phase req " << it->first << " -> " << it->second << std::endl; - if( it->second ){ - if( it->first.getKind()==EQUAL ){ - for( unsigned i=0; i<2; i++ ){ - if( it->first[i].getKind()==BOUND_VARIABLE ){ - unsigned j = i==0 ? 1 : 0; - if( !hasArg1( it->first[i], it->first[j] ) ){ - vars.push_back( it->first[i] ); - subs.push_back( it->first[j] ); - break; + }else if( body.getKind()==ITE && hasPol ){ + if( options::iteCondVarSplitQuant() ){ + Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl; + for( unsigned r=0; r<2; r++ ){ + //check if there is a variable elimination + Node b = r==0 ? body[0] : body[0].negate(); + QuantPhaseReq qpr( b ); + std::vector< Node > vars; + std::vector< Node > subs; + Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl; + for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ + Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl; + if( it->second ){ + if( it->first.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + if( it->first[i].getKind()==BOUND_VARIABLE ){ + unsigned j = i==0 ? 1 : 0; + if( !hasArg1( it->first[i], it->first[j] ) ){ + vars.push_back( it->first[i] ); + subs.push_back( it->first[j] ); + break; + } } } } } } - } - if( !vars.empty() ){ - //bool cpol = (r==1); - Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ); - //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - //pos = Rewriter::rewrite( pos ); - Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] ); - //Trace("ite-var-split-quant") << "Split ITE " << body << " into : " << std::endl; - //Trace("ite-var-split-quant") << " " << pos << std::endl; - //Trace("ite-var-split-quant") << " " << neg << std::endl; - return NodeManager::currentNM()->mkNode( AND, pos, neg ); + if( !vars.empty() ){ + //bool cpol = (r==1); + Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ); + //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + //pos = Rewriter::rewrite( pos ); + Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] ); + Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl; + Trace("quantifiers-rewrite-ite") << " " << pos << std::endl; + Trace("quantifiers-rewrite-ite") << " " << neg << std::endl; + return NodeManager::currentNM()->mkNode( AND, pos, neg ); + } } } } @@ -420,6 +497,26 @@ Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) return body; } +Node QuantifiersRewriter::computeProcessIte2( Node body ){ + if( body.getKind()==ITE ){ + if( options::iteDtTesterSplitQuant() ){ + Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl; + std::map< Node, Node > pcons; + std::map< Node, std::map< int, Node > > ncons; + std::vector< Node > conj; + computeDtTesterIteSplit( body, pcons, ncons, conj ); + Assert( !conj.empty() ); + if( conj.size()>1 ){ + Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl; + for( unsigned i=0; imkNode( AND, conj ); + } + } + } + return body; +} Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ @@ -1002,7 +1099,9 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption }else if( computeOption==COMPUTE_NNF ){ return options::nnfQuant(); }else if( computeOption==COMPUTE_PROCESS_ITE ){ - return options::iteCondVarSplitQuant() || options::simpleIteLiftQuant(); + return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); + }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){ + return options::iteDtTesterSplitQuant(); }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ @@ -1041,6 +1140,8 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp n = computeNNF( n ); }else if( computeOption==COMPUTE_PROCESS_ITE ){ n = computeProcessIte( n, true, true ); + }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){ + n = computeProcessIte2( n ); }else if( computeOption==COMPUTE_PRENEX ){ n = computePrenex( n, args, true ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 838eff57b..201a03737 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -40,12 +40,14 @@ private: static bool hasArg( std::vector< Node >& args, Node n ); static bool hasArg1( Node a, Node n ); 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 ); private: static Node computeElimSymbols( Node body ); static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); static Node computeNNF( Node body ); static Node computeProcessIte( Node body, bool hasPol, bool pol ); + static Node computeProcessIte2( Node body ); 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 ); @@ -57,6 +59,7 @@ private: COMPUTE_AGGRESSIVE_MINISCOPING, COMPUTE_NNF, COMPUTE_PROCESS_ITE, + COMPUTE_PROCESS_ITE_2, COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, //COMPUTE_FLATTEN_ARGS_UF, diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 84cb63617..8c99881d6 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1189,7 +1189,7 @@ bool TermDb::getTermOrder( Node a, Node b ) { Trace("aeq-debug2") << a << "...op..." << aop << std::endl; Trace("aeq-debug2") << b << "...op..." << bop << std::endl; if( aop==bop ){ - if( aop.getNumChildren()==bop.getNumChildren() ){ + if( a.getNumChildren()==b.getNumChildren() ){ for( unsigned i=0; i > d_cache; bool operator() (Node i, Node j) { + /* + //must consult cache since term order is partial? + std::map< Node, bool >::iterator it = d_cache[j].find( i ); + if( it!=d_cache[j].end() && it->second ){ + return false; + }else{ + bool ret = d_tdb->getTermOrder( i, j ); + d_cache[i][j] = ret; + return ret; + } + */ return d_tdb->getTermOrder( i, j ); } }; @@ -1238,6 +1250,7 @@ struct sortTermOrder { // - orders variables left to right // - if apply_torder, then sort direct subterms of commutative operators Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ) { + Trace("canon-term-debug") << "Get canonical term for " << n << std::endl; if( n.getKind()==BOUND_VARIABLE ){ std::map< TNode, TNode >::iterator it = subs.find( n ); if( it==subs.end() ){ @@ -1246,31 +1259,41 @@ Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_coun unsigned vn = var_count[tn]; var_count[tn]++; subs[n] = getCanonicalFreeVar( tn, vn ); + Trace("canon-term-debug") << "...allocate variable." << std::endl; return subs[n]; }else{ + Trace("canon-term-debug") << "...return variable in subs." << std::endl; return it->second; } }else if( n.getNumChildren()>0 ){ //collect children + Trace("canon-term-debug") << "Collect children" << std::endl; std::vector< Node > cchildren; for( unsigned i=0; imkNode( n.getKind(), cchildren ); + Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl; + Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren ); + Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl; + return ret; }else{ + Trace("canon-term-debug") << "...return 0-child term." << std::endl; return n; } } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index c202f9cb1..347aa83c4 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1163,7 +1163,6 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, } Trace("internal-rep-select") << " } " << std::endl; int r_best_score = -1; - TypeNode v_tn = f[0][index].getType(); for( size_t i=0; i