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;;
}
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
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
--- /dev/null
+#!/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"
+++ /dev/null
-#!/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"
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 */
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 )
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
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
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
+ 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") {
}
}
+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 */
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;
++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);
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);
}
}
+
+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 );
+ }
}
}
}
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; i<conj.size(); i++ ){
+ Trace("quantifiers-rewrite-ite") << " " << conj[i] << std::endl;
+ }
+ return NodeManager::currentNM()->mkNode( AND, conj );
+ }
+ }
+ }
+ return body;
+}
Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
}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 ){
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 ){
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 );
COMPUTE_AGGRESSIVE_MINISCOPING,
COMPUTE_NNF,
COMPUTE_PROCESS_ITE,
+ COMPUTE_PROCESS_ITE_2,
COMPUTE_PRENEX,
COMPUTE_VAR_ELIMINATION,
//COMPUTE_FLATTEN_ARGS_UF,
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<a.getNumChildren(); i++ ){
if( a[i]!=b[i] ){
//first distinct child determines the ordering
struct sortTermOrder {
TermDb* d_tdb;
+ //std::map< Node, std::map< Node, bool > > 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 );
}
};
// - 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() ){
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; i<n.getNumChildren(); i++ ){
cchildren.push_back( n[i] );
}
//if applicable, first sort by term order
if( apply_torder && isComm( n.getKind() ) ){
+ Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl;
sortTermOrder sto;
sto.d_tdb = this;
std::sort( cchildren.begin(), cchildren.end(), sto );
}
//now make canonical
+ Trace("canon-term-debug") << "Make canonical children" << std::endl;
for( unsigned i=0; i<cchildren.size(); i++ ){
cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder );
}
- if( n.hasOperator() ){
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl;
cchildren.insert( cchildren.begin(), n.getOperator() );
}
- return NodeManager::currentNM()->mkNode( 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;
}
}
}
Trace("internal-rep-select") << " } " << std::endl;
int r_best_score = -1;
- TypeNode v_tn = f[0][index].getType();
for( size_t i=0; i<eqc.size(); i++ ){
int score = getRepScore( eqc[i], f, index, v_tn );
if( score!=-2 ){
projects / cvc5.git / commitdiff