diff options
27 files changed, 2068 insertions, 312 deletions
diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 67ce3988a..bbee2d49b 100755 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -3,15 +3,14 @@ ; SMT syntax and semantics (not theory-specific) ; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; depends on sat.plf (declare formula type) (declare th_holds (! f formula type)) -; constants +; standard logic definitions (declare true formula) (declare false formula) - -; logical connectives (declare not (! f formula formula)) (declare and (! f1 formula (! f2 formula formula))) (declare or (! f1 formula (! f2 formula formula))) @@ -21,24 +20,19 @@ (declare ifte (! b formula (! f1 formula (! f2 formula formula)))) ; terms -(declare sort type) ; sort in the theory -(declare arrow (! s1 sort (! s2 sort sort))) ; function constructor - +(declare sort type) (declare term (! t sort type)) ; declared terms in formula -(declare apply (! s1 sort - (! s2 sort - (! t1 (term (arrow s1 s2)) - (! t2 (term s1) - (term s2)))))) - +; standard definitions for =, ite, let and flet +(declare = (! s sort + (! x (term s) + (! y (term s) + formula)))) (declare ite (! s sort (! f formula (! t1 (term s) (! t2 (term s) (term s)))))) - -; let/flet (declare let (! s sort (! t (term s) (! f (! v (term s) formula) @@ -47,38 +41,52 @@ (! f2 (! v formula formula) formula))) -; predicates -(declare = (! s sort - (! x (term s) - (! y (term s) - formula)))) - -; To avoid duplicating some of the rules (e.g., cong), we will view -; applications of predicates as terms of sort "Bool". +; We view applications of predicates as terms of sort "Bool". ; Such terms can be injected as atomic formulas using "p_app". - (declare Bool sort) ; the special sort for predicates (declare p_app (! x (term Bool) formula)) ; propositional application of term ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; Examples +; +; CNF Clausification +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; an example of "(p1 or p2(0)) and t1=t2(1)" -;(! p1 (term Bool) -;(! p2 (term (arrow Int Bool)) -;(! t1 (term Int) -;(! t2 (term (arrow Int Int)) -;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0))) -; (= _ t1 (apply _ _ t2 1)))) -; ... +; binding between an LF var and an (atomic) formula +(declare atom (! v var (! p formula type))) -; another example of "p3(a,b)" -;(! a (term Int) -;(! b (term Int) -;(! p3 (term (arrow Int (arrow Int Bool))) ; arrow is right assoc. -;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc. -; ... +(declare decl_atom + (! f formula + (! u (! v var + (! a (atom v f) + (holds cln))) + (holds cln)))) + +; clausify a formula directly +(declare clausify_form + (! f formula + (! v var + (! a (atom v f) + (! u (th_holds f) + (holds (clc (pos v) cln))))))) + +(declare clausify_form_not + (! f formula + (! v var + (! a (atom v f) + (! u (th_holds (not f)) + (holds (clc (neg v) cln))))))) + +(declare clausify_false + (! u (th_holds false) + (holds cln))) + +(declare th_let_pf + (! f formula + (! u (th_holds f) + (! u2 (! v (th_holds f) (holds cln)) + (holds cln))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -261,13 +269,41 @@ (! u2 (th_holds (not (ifte (not a) b c))) (th_holds (not c)))))))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; For theory lemmas +; - make a series of assumptions and then derive a contradiction (or false) +; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false" +; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn" +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(declare ast + (! v var + (! f formula + (! C clause + (! r (atom v f) ;this is specified + (! u (! o (th_holds f) + (holds C)) + (holds (clc (neg v) C)))))))) + +(declare asf + (! v var + (! f formula + (! C clause + (! r (atom v f) + (! u (! o (th_holds (not f)) + (holds C)) + (holds (clc (pos v) C)))))))) + + -;; How to do CNF for disjunctions of theory literals. +;; Example: ;; -;; Given theory literals F1....Fn, and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))). +;; Given theory literals (F1....Fn), and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))). ;; -;; We introduce atoms a1...an for literals F1...Fn, mapping them to boolean literals v1...vn. +;; We introduce atoms (a1,...,an) to map boolean literals (v1,...,vn) top literals (F1,...,Fn). ;; Do this at the beginning of the proof: ;; ;; (decl_atom F1 (\ v1 (\ a1 @@ -275,7 +311,7 @@ ;; .... ;; (decl_atom Fn (\ vn (\ an ;; -;; Our input A is clausified by the following proof: +;; A is then clausified by the following proof: ;; ;;(satlem _ _ ;;(asf _ _ _ a1 (\ l1 @@ -294,7 +330,7 @@ ;; ;; We now have the free variable C, which should be the clause (v1 V ... V vn). ;; -;; We also need to consider the polarity of literals, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))). +;; Polarity of literals should be considered, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))). ;; Where necessary, we use "ast" instead of "asf", introduce negations by "not_not_intro" for pattern matching, and flip ;; the arguments of contra: ;; @@ -311,3 +347,5 @@ ;;))))))) (\ C ;; ;; C should be the clause (~v1 V v2 V ~v3 ) + + diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf new file mode 100755 index 000000000..6e0e6438d --- /dev/null +++ b/proofs/signatures/th_arrays.plf @@ -0,0 +1,53 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Theory of Arrays
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; depdends on : th_base.plf
+
+; sorts
+
+(declare array (! s1 sort (! s2 sort sort))) ; s1 is index, s2 is element
+
+; functions
+(declare write (! s1 sort
+ (! s2 sort
+ (! t1 (term (array s1 s2))
+ (! t2 (term s1)
+ (! t3 (term s2)
+ (term (array s1 s2))))))))
+(declare read (! s1 sort
+ (! s2 sort
+ (! t1 (term (array s1 s2))
+ (! t2 (term s1)
+ (term s2))))))
+
+; inference rules
+(declare row1 (! s1 sort
+ (! s2 sort
+ (! t1 (term (array s1 s2))
+ (! t2 (term s1)
+ (! t3 (term s2)
+ (th_holds (= _ (read (write t1 t2 t3) t2) t3))))))))
+
+
+(declare row (! s1 sort
+ (! s2 sort
+ (! t1 (term (array s1 s2))
+ (! t2 (term s1)
+ (! t3 (term s1)
+ (! t4 (term s2)
+ (! u (th_holds (not (= _ t2 t3)))
+ (th_holds (= _ (read (write t1 t2 t4) t3) (read t1 t3))))))))))
+
+(declare ext (! s1 sort
+ (! s2 sort
+ (! f formula
+ (! t1 (term (array s1 s2))
+ (! t2 (term (array s1 s2))
+ (! u (th_holds (not (= _ t1 t2)))
+ (! u1 (! k (term s1)
+ (! u2 (th_holds (not (= _ (read t1 k) (read t2 k))))
+ (th_holds f)))
+ (th_holds f)))))))))
+
\ No newline at end of file diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf index 7b0b086dc..977409b6a 100755 --- a/proofs/signatures/th_base.plf +++ b/proofs/signatures/th_base.plf @@ -1,80 +1,28 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; -; Atomization / Clausification -; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -; binding between an LF var and an (atomic) formula -(declare atom (! v var (! p formula type))) - -(declare decl_atom - (! f formula - (! u (! v var - (! a (atom v f) - (holds cln))) - (holds cln)))) - -; direct clausify -(declare clausify_form - (! f formula - (! v var - (! a (atom v f) - (! u (th_holds f) - (holds (clc (pos v) cln))))))) - -(declare clausify_form_not - (! f formula - (! v var - (! a (atom v f) - (! u (th_holds (not f)) - (holds (clc (neg v) cln))))))) - -(declare clausify_false - (! u (th_holds false) - (holds cln))) -(declare th_let_pf - (! f formula - (! u (th_holds f) - (! u2 (! v (th_holds f) (holds cln)) - (holds cln))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; -; Theory reasoning -; - make a series of assumptions and then derive a contradiction (or false) -; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false" -; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn" +; Theory of Equality and Congruence Closure ; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; depends on : smt.plf -(declare ast - (! v var - (! f formula - (! C clause - (! r (atom v f) ;this is specified - (! u (! o (th_holds f) - (holds C)) - (holds (clc (neg v) C)))))))) +; sorts : -(declare asf - (! v var - (! f formula - (! C clause - (! r (atom v f) - (! u (! o (th_holds (not f)) - (holds C)) - (holds (clc (pos v) C)))))))) +(declare arrow (! s1 sort (! s2 sort sort))) ; function constructor -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; -; Theory of Equality and Congruence Closure -; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; functions : -; temporary : -(declare trust (th_holds false)) +(declare apply (! s1 sort + (! s2 sort + (! t1 (term (arrow s1 s2)) + (! t2 (term s1) + (term s2)))))) + + +; inference rules : + +(declare trust (th_holds false)) ; temporary (declare refl (! s sort @@ -105,3 +53,21 @@ (! u2 (th_holds (= _ a2 b2)) (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2)))))))))))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; Examples + +; an example of "(p1 or p2(0)) and t1=t2(1)" +;(! p1 (term Bool) +;(! p2 (term (arrow Int Bool)) +;(! t1 (term Int) +;(! t2 (term (arrow Int Int)) +;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0))) +; (= _ t1 (apply _ _ t2 1)))) +; ... + +; another example of "p3(a,b)" +;(! a (term Int) +;(! b (term Int) +;(! p3 (term (arrow Int (arrow Int Bool))) ; arrow is right assoc. +;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc. +; ... diff --git a/src/Makefile.am b/src/Makefile.am index c765d325a..eda6acd6b 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -291,6 +291,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/relevant_domain.cpp \ theory/quantifiers/symmetry_breaking.h \ theory/quantifiers/symmetry_breaking.cpp \ + theory/quantifiers/qinterval_builder.h \ + theory/quantifiers/qinterval_builder.cpp \ theory/quantifiers/options_handlers.h \ theory/rewriterules/theory_rewriterules_rules.h \ theory/rewriterules/theory_rewriterules_rules.cpp \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f26456cae..539622877 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -771,7 +771,7 @@ void SmtEngine::finishInit() { setTimeLimit(options::cumulativeMillisecondLimit(), true); } - PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); + PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); } void SmtEngine::finalOptionsAreSet() { @@ -1144,13 +1144,17 @@ void SmtEngine::setLogicInternal() throw() { } if ( ! options::fmfInstGen.wasSetByUser()) { //if full model checking is on, disable inst-gen techniques - if( options::fmfFullModelCheck() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ options::fmfInstGen.set( false ); + }else{ + options::fmfInstGen.set( true ); } } if ( options::fmfBoundInt() ){ - //if bounded integers are set, must use full model check for MBQI - options::fmfFullModelCheck.set( true ); + if( options::mbqiMode()!=quantifiers::MBQI_NONE ){ + //if bounded integers are set, must use full model check for MBQI + options::mbqiMode.set( quantifiers::MBQI_FMC ); + } } if( options::ufssSymBreak() ){ options::sortInference.set( true ); @@ -3309,7 +3313,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc // Ensure expr is type-checked at this point. ensureBoolean(e); // Give it to proof manager - PROOF( ProofManager::currentPM()->addAssertion(e); ); + PROOF( ProofManager::currentPM()->addAssertion(e); ); } // check to see if a postsolve() is pending @@ -3390,7 +3394,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept // Ensure that the expression is type-checked at this point, and Boolean ensureBoolean(e); // Give it to proof manager - PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); ); + PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); ); // check to see if a postsolve() is pending if(d_needPostsolve) { @@ -3455,7 +3459,7 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log finalOptionsAreSet(); doPendingPops(); - PROOF( ProofManager::currentPM()->addAssertion(ex); ); + PROOF( ProofManager::currentPM()->addAssertion(ex); ); Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index bda124e96..c94775aec 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -16,6 +16,8 @@ #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/full_model_check.h" +#include "theory/quantifiers/qinterval_builder.h" #define USE_INDEX_ORDERING @@ -27,8 +29,9 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::quantifiers::fmcheck; -FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : TheoryModel( c, name, true ), -d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){ +FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) : +TheoryModel( c, name, true ), +d_qe( qe ), d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){ } @@ -66,16 +69,23 @@ Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) { } void FirstOrderModel::initialize( bool considerAxioms ) { - processInitialize(); + processInitialize( true ); //this is called after representatives have been chosen and the equality engine has been built //for each quantifier, collect all operators we care about for( int i=0; i<getNumAssertedQuantifiers(); i++ ){ Node f = getAssertedQuantifier( i ); + processInitializeQuantifier( f ); + if( d_quant_var_id.find( f )==d_quant_var_id.end() ){ + for(unsigned i=0; i<f[0].getNumChildren(); i++){ + d_quant_var_id[f][f[0][i]] = i; + } + } if( considerAxioms || !f.hasAttribute(AxiomAttribute()) ){ //initialize relevant models within bodies of all quantifiers initializeModelForTerm( f[1] ); } } + processInitialize( false ); } void FirstOrderModel::initializeModelForTerm( Node n ){ @@ -85,14 +95,30 @@ void FirstOrderModel::initializeModelForTerm( Node n ){ } } -FirstOrderModelIG::FirstOrderModelIG(context::Context* c, std::string name) : FirstOrderModel(c,name) { +Node FirstOrderModel::getSomeDomainElement(TypeNode tn){ + //check if there is even any domain elements at all + if (!d_rep_set.hasType(tn)) { + Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl; + Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn); + d_rep_set.add(mbt); + }else if( d_rep_set.d_type_reps[tn].size()==0 ){ + Message() << "empty reps" << std::endl; + exit(0); + } + return d_rep_set.d_type_reps[tn][0]; +} + +FirstOrderModelIG::FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name) : +FirstOrderModel(qe, c,name) { } -void FirstOrderModelIG::processInitialize(){ - //rebuild models - d_uf_model_tree.clear(); - d_uf_model_gen.clear(); +void FirstOrderModelIG::processInitialize( bool ispre ){ + if( ispre ){ + //rebuild models + d_uf_model_tree.clear(); + d_uf_model_gen.clear(); + } } void FirstOrderModelIG::processInitializeModelForTerm( Node n ){ @@ -513,10 +539,8 @@ Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & ar - - FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) : -FirstOrderModel(c, name), d_qe(qe){ +FirstOrderModel(qe, c, name){ } @@ -552,19 +576,21 @@ Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & a return d_models[n.getOperator()]->evaluate(this, args); } -void FirstOrderModelFmc::processInitialize() { - if( options::fmfFmcInterval() && intervalOp.isNull() ){ - std::vector< TypeNode > types; - for(unsigned i=0; i<2; i++){ - types.push_back(NodeManager::currentNM()->integerType()); +void FirstOrderModelFmc::processInitialize( bool ispre ) { + if( ispre ){ + if( options::fmfFmcInterval() && intervalOp.isNull() ){ + std::vector< TypeNode > types; + for(unsigned i=0; i<2; i++){ + types.push_back(NodeManager::currentNM()->integerType()); + } + TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->integerType() ); + intervalOp = NodeManager::currentNM()->mkSkolem( "interval_$$", typ, "op representing interval" ); } - TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->integerType() ); - intervalOp = NodeManager::currentNM()->mkSkolem( "interval_$$", typ, "op representing interval" ); - } - for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){ - it->second->reset(); + for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){ + it->second->reset(); + } + d_model_basis_rep.clear(); } - d_model_basis_rep.clear(); } void FirstOrderModelFmc::processInitializeModelForTerm(Node n) { @@ -575,19 +601,6 @@ void FirstOrderModelFmc::processInitializeModelForTerm(Node n) { } } -Node FirstOrderModelFmc::getSomeDomainElement(TypeNode tn){ - //check if there is even any domain elements at all - if (!d_rep_set.hasType(tn)) { - Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl; - Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn); - d_rep_set.d_type_reps[tn].push_back(mbt); - }else if( d_rep_set.d_type_reps[tn].size()==0 ){ - Message() << "empty reps" << std::endl; - exit(0); - } - return d_rep_set.d_type_reps[tn][0]; -} - bool FirstOrderModelFmc::isStar(Node n) { return n==getStar(n.getType()); @@ -684,3 +697,163 @@ bool FirstOrderModelFmc::isInRange( Node v, Node i ) { return v==i; } } + + +FirstOrderModelQInt::FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name) : +FirstOrderModel(qe, c, name) { + +} + +void FirstOrderModelQInt::processInitialize( bool ispre ) { + if( !ispre ){ + Trace("qint-debug") << "Process initialize" << std::endl; + for( std::map<Node, QIntDef * >::iterator it = d_models.begin(); it != d_models.end(); ++it ) { + Node op = it->first; + TypeNode tno = op.getType(); + Trace("qint-debug") << " Init " << op << " " << tno << std::endl; + for( unsigned i=0; i<tno.getNumChildren(); i++) { + //make sure a representative of the type exists + if( !d_rep_set.hasType( tno[i] ) ){ + Node e = getSomeDomainElement( tno[i] ); + Trace("qint-debug") << " * Initialize type " << tno[i] << ", add "; + Trace("qint-debug") << e << " " << e.getType() << std::endl; + //d_rep_set.add( e ); + } + } + } + } +} + +Node FirstOrderModelQInt::getFunctionValue(Node op, const char* argPrefix ) { + Trace("qint-debug") << "Get function value for " << op << std::endl; + TypeNode type = op.getType(); + std::vector< Node > vars; + for( size_t i=0; i<type.getNumChildren()-1; i++ ){ + std::stringstream ss; + ss << argPrefix << (i+1); + Node b = NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ); + vars.push_back( b ); + } + Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); + Node curr = d_models[op]->getFunctionValue( this, vars ); + Node fv = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); + Trace("qint-debug") << "Return " << fv << std::endl; + return fv; +} + +Node FirstOrderModelQInt::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) { + Debug("qint-debug") << "get curr uf value " << n << std::endl; + return d_models[n]->evaluate( this, args ); +} + +void FirstOrderModelQInt::processInitializeModelForTerm(Node n) { + Debug("qint-debug") << "process init " << n << " " << n.getKind() << std::endl; + + if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ + Node op = n.getKind()==APPLY_UF ? n.getOperator() : n; + if( d_models.find(op)==d_models.end()) { + Debug("qint-debug") << "init model for " << op << std::endl; + d_models[op] = new QIntDef; + } + } +} + +Node FirstOrderModelQInt::getUsedRepresentative( Node n ) { + if( hasTerm( n ) ){ + if( n.getType().isBoolean() ){ + return areEqual(n, d_true) ? d_true : d_false; + }else{ + return getRepresentative( n ); + } + }else{ + Trace("qint-debug") << "Get rep " << n << " " << n.getType() << std::endl; + Assert( d_rep_set.hasType( n.getType() ) && !d_rep_set.d_type_reps[n.getType()].empty() ); + return d_rep_set.d_type_reps[n.getType()][0]; + } +} + +void FirstOrderModelQInt::processInitializeQuantifier( Node q ) { + if( d_var_order.find( q )==d_var_order.end() ){ + d_var_order[q] = new QuantVarOrder( q ); + d_var_order[q]->debugPrint("qint-var-order"); + Trace("qint-var-order") << std::endl; + } +} +unsigned FirstOrderModelQInt::getOrderedNumVars( Node q ) { + //return q[0].getNumChildren(); + return d_var_order[q]->getNumVars(); +} + +TypeNode FirstOrderModelQInt::getOrderedVarType( Node q, int i ) { + //return q[0][i].getType(); + return d_var_order[q]->getVar( i ).getType(); +} + +int FirstOrderModelQInt::getOrderedVarNumToVarNum( Node q, int i ) { + return getVariableId( q, d_var_order[q]->getVar( i ) ); +} + +bool FirstOrderModelQInt::isLessThan( Node v1, Node v2 ) { + Assert( !v1.isNull() ); + Assert( !v2.isNull() ); + if( v1.getType().isSort() ){ + Assert( getRepId( v1 )!=-1 ); + Assert( getRepId( v2 )!=-1 ); + int rid1 = d_rep_id[v1]; + int rid2 = d_rep_id[v2]; + return rid1<rid2; + }else{ + return false; + } +} + +Node FirstOrderModelQInt::getMin( Node v1, Node v2 ) { + return isLessThan( v1, v2 ) ? v1 : v2; +} + +Node FirstOrderModelQInt::getMax( Node v1, Node v2 ) { + return isLessThan( v1, v2 ) ? v2 : v1; +} + +Node FirstOrderModelQInt::getMaximum( TypeNode tn ) { + return d_max[tn]; +} + +Node FirstOrderModelQInt::getNext( TypeNode tn, Node v ) { + if( v.isNull() ){ + return d_min[tn]; + }else{ + Assert( getRepId( v )!=-1 ); + int rid = d_rep_id[v]; + if( rid==(int)(d_rep_set.d_type_reps[tn].size()-1) ){ + Assert( false ); + return Node::null(); + }else{ + return d_rep_set.d_type_reps[tn][ rid+1 ]; + } + } +} +Node FirstOrderModelQInt::getPrev( TypeNode tn, Node v ) { + if( v.isNull() ){ + Assert( false ); + return Node::null(); + }else{ + Assert( getRepId( v )!=-1 ); + int rid = d_rep_id[v]; + if( rid==0 ){ + return Node::null(); + }else{ + return d_rep_set.d_type_reps[tn][ rid-1 ]; + } + } +} + +bool FirstOrderModelQInt::doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur ) { + Trace("qint-debug2") << "doMeet " << l1 << "..." << u1 << " with " << l2 << "..." << u2 << std::endl; + Assert( !u1.isNull() ); + Assert( !u2.isNull() ); + lr = l1.isNull() ? l2 : ( l2.isNull() ? l1 : getMax( l1, l2 ) ); + ur = getMin( u1, u2 ); + //return lr==ur || lr.isNull() || isLessThan( lr, ur ); + return lr.isNull() || isLessThan( lr, ur ); +} diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index b5bdff9ee..ab3a1aa52 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -33,16 +33,21 @@ class FirstOrderModelIG; namespace fmcheck { class FirstOrderModelFmc; } +class FirstOrderModelQInt; class FirstOrderModel : public TheoryModel { -private: +protected: + /** quant engine */ + QuantifiersEngine * d_qe; /** whether an axiom is asserted */ context::CDO< bool > d_axiom_asserted; /** list of quantifiers asserted in the current context */ context::CDList<Node> d_forall_asserts; /** is model set */ context::CDO< bool > d_isModelSet; + /** get variable id */ + std::map< Node, std::map< Node, int > > d_quant_var_id; /** get current model value */ virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0; public: //for Theory Quantifiers: @@ -57,20 +62,28 @@ public: //for Theory Quantifiers: /** initialize model for term */ void initializeModelForTerm( Node n ); virtual void processInitializeModelForTerm( Node n ) = 0; + virtual void processInitializeQuantifier( Node q ) {} public: - FirstOrderModel( context::Context* c, std::string name ); + FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ); virtual ~FirstOrderModel(){} virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; } virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; } + virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; } // initialize the model void initialize( bool considerAxioms = true ); - virtual void processInitialize() = 0; + virtual void processInitialize( bool ispre ) = 0; /** mark model set */ void markModelSet() { d_isModelSet = true; } /** is model set */ bool isModelSet() { return d_isModelSet; } /** get current model value */ Node getCurrentModelValue( Node n, bool partial = false ); + /** get variable id */ + int getVariableId(Node f, Node n) { + return d_quant_var_id.find( f )!=d_quant_var_id.end() ? d_quant_var_id[f][n] : -1; + } + /** get some domain element */ + Node getSomeDomainElement(TypeNode tn); };/* class FirstOrderModel */ @@ -93,10 +106,10 @@ private: Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ); //the following functions are for evaluating quantifier bodies public: - FirstOrderModelIG(context::Context* c, std::string name); + FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name); FirstOrderModelIG * asFirstOrderModelIG() { return this; } // initialize the model - void processInitialize(); + void processInitialize( bool ispre ); //for initialize model void processInitializeModelForTerm( Node n ); /** reset evaluation */ @@ -128,8 +141,6 @@ class FirstOrderModelFmc : public FirstOrderModel { friend class FullModelChecker; private: - /** quant engine */ - QuantifiersEngine * d_qe; /** models for UF */ std::map<Node, Def * > d_models; std::map<TypeNode, Node > d_model_basis_rep; @@ -143,8 +154,7 @@ public: FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name); FirstOrderModelFmc * asFirstOrderModelFmc() { return this; } // initialize the model - void processInitialize(); - + void processInitialize( bool ispre ); Node getFunctionValue(Node op, const char* argPrefix ); bool isStar(Node n); @@ -152,7 +162,6 @@ public: Node getStarElement(TypeNode tn); bool isModelBasisTerm(Node n); Node getModelBasisTerm(TypeNode tn); - Node getSomeDomainElement(TypeNode tn); bool isInterval(Node n); Node getInterval( Node lb, Node ub ); bool isInRange( Node v, Node i ); @@ -161,6 +170,50 @@ public: } +class QIntDef; +class QuantVarOrder; +class FirstOrderModelQInt : public FirstOrderModel +{ + friend class QIntervalBuilder; +private: + /** uf op to some representation */ + std::map<Node, QIntDef * > d_models; + /** representatives to ids */ + std::map< Node, int > d_rep_id; + std::map< TypeNode, Node > d_min; + std::map< TypeNode, Node > d_max; + /** quantifiers to information regarding variable ordering */ + std::map<Node, QuantVarOrder * > d_var_order; + /** get current model value */ + Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ); + void processInitializeModelForTerm(Node n); +public: + FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name); + FirstOrderModelQInt * asFirstOrderModelQInt() { return this; } + void processInitialize( bool ispre ); + Node getFunctionValue(Node op, const char* argPrefix ); + + Node getUsedRepresentative( Node n ); + int getRepId( Node n ) { return d_rep_id.find( n )==d_rep_id.end() ? -1 : d_rep_id[n]; } + bool isLessThan( Node v1, Node v2 ); + Node getMin( Node v1, Node v2 ); + Node getMax( Node v1, Node v2 ); + Node getMinimum( TypeNode tn ) { return getNext( tn, Node::null() ); } + Node getMaximum( TypeNode tn ); + bool isMinimum( Node n ) { return n==getMinimum( n.getType() ); } + bool isMaximum( Node n ) { return n==getMaximum( n.getType() ); } + Node getNext( TypeNode tn, Node v ); + Node getPrev( TypeNode tn, Node v ); + bool doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur ); + QuantVarOrder * getVarOrder( Node q ) { return d_var_order[q]; } + + void processInitializeQuantifier( Node q ) ; + unsigned getOrderedNumVars( Node q ); + TypeNode getOrderedVarType( Node q, int i ); + int getOrderedVarNumToVarNum( Node q, int i ); +}; + + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 2f32ec5e6..174e26a5a 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -588,7 +588,6 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, std::vector< TypeNode > types; for(unsigned i=0; i<f[0].getNumChildren(); i++){ types.push_back(f[0][i].getType()); - d_quant_var_id[f][f[0][i]] = i; } TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() ); Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" ); @@ -599,7 +598,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, initializeType( fmfmc, f[0][i].getType() ); } - if( !options::fmfModelBasedInst() ){ + if( options::mbqiMode()==MBQI_NONE ){ //just exhaustive instantiate Node c = mkCondDefault( fmfmc, f ); d_quant_models[f].addEntry( fmfmc, c, d_false ); @@ -958,8 +957,8 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def }else{ TypeNode tn = eq[0].getType(); if( tn.isSort() ){ - int j = getVariableId(f, eq[0]); - int k = getVariableId(f, eq[1]); + int j = fm->getVariableId(f, eq[0]); + int k = fm->getVariableId(f, eq[1]); if( !fm->d_rep_set.hasType( tn ) ){ getSomeDomainElement( fm, tn ); //to verify the type is initialized } @@ -977,7 +976,7 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def } void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v) { - int j = getVariableId(f, v); + int j = fm->getVariableId(f, v); for (unsigned i=0; i<dc.d_cond.size(); i++) { Node val = dc.d_value[i]; if( val.isNull() ){ @@ -1074,7 +1073,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, Trace("fmc-uf-process") << "Process " << v << std::endl; bool bind_var = false; if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){ - int j = getVariableId(f, v); + int j = fm->getVariableId(f, v); Trace("fmc-uf-process") << v << " is variable #" << j << std::endl; if (!fm->isStar(cond[j+1]) && !fm->isInterval(cond[j+1])) { v = cond[j+1]; @@ -1084,7 +1083,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, } if (bind_var) { Trace("fmc-uf-process") << "bind variable..." << std::endl; - int j = getVariableId(f, v); + int j = fm->getVariableId(f, v); if( fm->isStar(cond[j+1]) ){ for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) { cond[j+1] = it->first; diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 606392831..db5abb01e 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -92,7 +92,6 @@ protected: std::map<Node, Node > d_quant_cond; std::map< TypeNode, Node > d_array_cond; std::map< Node, Node > d_array_term_cond; - std::map<Node, std::map< Node, int > > d_quant_var_id; std::map<Node, std::vector< int > > d_star_insts; void initializeType( FirstOrderModelFmc * fm, TypeNode tn ); Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); @@ -138,7 +137,6 @@ public: bool optBuildAtFullModel(); - int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; } void debugPrintCond(const char * tr, Node n, bool dispStar = false); void debugPrint(const char * tr, Node n, bool dispStar = false); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index ea6f2d775..468c78978 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -44,7 +44,7 @@ bool QModelBuilder::isQuantifierActive( Node f ) { bool QModelBuilder::optUseModel() { - return options::fmfModelBasedInst() || options::fmfBoundInt(); + return options::mbqiMode()!=MBQI_NONE || options::fmfBoundInt(); } void QModelBuilder::debugModel( FirstOrderModel* fm ){ @@ -124,6 +124,7 @@ Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std:: void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { FirstOrderModel* f = (FirstOrderModel*)m; FirstOrderModelIG* fm = f->asFirstOrderModelIG(); + Trace("model-engine-debug") << "Process build model, fullModel = " << fullModel << " " << optUseModel() << std::endl; if( fullModel ){ Assert( d_curr_model==fm ); //update models @@ -145,7 +146,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { reset( fm ); //only construct first order model if optUseModel() is true if( optUseModel() ){ - Trace("model-engine-debug") << "Initializing quantifiers..." << std::endl; + Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl; //check if any quantifiers are un-initialized for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); @@ -397,7 +398,6 @@ bool QModelBuilderIG::isTermActive( Node n ){ //do exhaustive instantiation bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { if( optUseModel() ){ - RepSetIterator riter( d_qe, &(d_qe->getModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel(); @@ -456,7 +456,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i d_statistics.d_eval_lits += fmig->d_eval_lits; d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown; } - Trace("inst-fmf-ei") << "Finished: " << std::endl; + Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl; Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas << std::endl; Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas << std::endl; if( d_addedLemmas>1000 ){ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 99f5e8df6..5006a8a61 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -21,6 +21,8 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/full_model_check.h" +#include "theory/quantifiers/qinterval_builder.h" using namespace std; using namespace CVC4; @@ -34,11 +36,18 @@ using namespace CVC4::theory::inst; ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule( qe ){ - if( options::fmfFullModelCheck() || options::fmfBoundInt() ){ + Trace("model-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; + if( options::mbqiMode()==MBQI_FMC || options::fmfBoundInt() ){ + Trace("model-engine-debug") << "...make fmc builder." << std::endl; d_builder = new fmcheck::FullModelChecker( c, qe ); - }else if( options::fmfNewInstGen() ){ + }else if( options::mbqiMode()==MBQI_INTERVAL ){ + Trace("model-engine-debug") << "...make interval builder." << std::endl; + d_builder = new QIntervalBuilder( c, qe ); + }else if( options::mbqiMode()==MBQI_INST_GEN ){ + Trace("model-engine-debug") << "...make inst-gen builder." << std::endl; d_builder = new QModelBuilderInstGen( c, qe ); }else{ + Trace("model-engine-debug") << "...make default model builder." << std::endl; d_builder = new QModelBuilderDefault( c, qe ); } @@ -203,7 +212,7 @@ int ModelEngine::checkModel(){ } Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; - int e_max = options::fmfFullModelCheck() && options::fmfModelBasedInst() ? 2 : 1; + int e_max = options::mbqiMode()==MBQI_FMC ? 2 : 1; for( int e=0; e<e_max; e++) { if (d_addedLemmas==0) { for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 0c3c74b5f..fcbba7aee 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -20,7 +20,6 @@ #include "theory/quantifiers_engine.h" #include "theory/quantifiers/model_builder.h" #include "theory/theory_model.h" -#include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/relevant_domain.h" namespace CVC4 { diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp index 7da3b150f..10185914e 100644 --- a/src/theory/quantifiers/modes.cpp +++ b/src/theory/quantifiers/modes.cpp @@ -77,5 +77,28 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::AxiomInstMode m return out; } +std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) { + switch(mode) { + case theory::quantifiers::MBQI_DEFAULT: + out << "MBQI_DEFAULT"; + break; + case theory::quantifiers::MBQI_NONE: + out << "MBQI_NONE"; + break; + case theory::quantifiers::MBQI_INST_GEN: + out << "MBQI_INST_GEN"; + break; + case theory::quantifiers::MBQI_FMC: + out << "MBQI_FMC"; + break; + case theory::quantifiers::MBQI_INTERVAL: + out << "MBQI_INTERVAL"; + break; + default: + out << "MbqiMode!UNKNOWN"; + } + return out; +} + }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index edf9c78fe..7c4cb3651 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -55,6 +55,22 @@ typedef enum { AXIOM_INST_MODE_PRIORITY, } AxiomInstMode; +typedef enum { + /** default, mbqi from CADE 24 paper */ + MBQI_DEFAULT, + /** no mbqi */ + MBQI_NONE, + /** implementation that mimics inst-gen */ + MBQI_INST_GEN, + /** mbqi from Section 5.4.2 of AJR thesis */ + MBQI_FMC, + /** mbqi with integer intervals */ + //MBQI_FMC_INTERVAL, + /** mbqi with interval abstraction of uninterpreted sorts */ + MBQI_INTERVAL, +} MbqiMode; + + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 1eb98e7b7..f485b981c 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -95,11 +95,9 @@ option internalReps /--disable-quant-internal-reps bool :default true option finiteModelFind --finite-model-find bool :default false use finite model finding heuristic for quantifier instantiation -option fmfModelBasedInst /--disable-fmf-mbqi bool :default true - disable model-based quantifier instantiation for finite model finding +option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" + choose mode for model-based quantifier instantiation -option fmfFullModelCheck --fmf-fmc bool :default false :read-write - enable full model check for finite model finding option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding option fmfFmcCoverSimplify /--disable-fmf-fmc-cover-simplify bool :default true @@ -115,8 +113,6 @@ option fmfInstEngine --fmf-inst-engine bool :default false use instantiation engine in conjunction with finite model finding option fmfRelevantDomain --fmf-relevant-domain bool :default false use relevant domain computation, similar to complete instantiation (Ge, deMoura 09) -option fmfNewInstGen --fmf-new-inst-gen bool :default false - use new inst gen technique for answering sat without exhaustive instantiation option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true enable Inst-Gen instantiation techniques for finite model finding (default) /disable Inst-Gen instantiation techniques for finite model finding diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 410578af0..a119bcaf6 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -73,6 +73,28 @@ priority \n\ \n\ "; +static const std::string mbqiModeHelp = "\ +Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ +\n\ +default \n\ ++ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\ + model finding paper.\n\ +\n\ +none \n\ ++ Disable model-based quantifier instantiation.\n\ +\n\ +instgen \n\ ++ Use instantiation algorithm that mimics Inst-Gen calculus. \n\ +\n\ +fmc \n\ ++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability. \n\ + Modulo Theories.\n\ +\n\ +interval \n\ ++ Use algorithm that abstracts domain elements as intervals. \n\ +\n\ +"; + inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { return INST_WHEN_PRE_FULL; @@ -135,6 +157,30 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar } } +inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "default") { + return MBQI_DEFAULT; + } else if(optarg == "none") { + return MBQI_NONE; + } else if(optarg == "instgen") { + return MBQI_INST_GEN; + } else if(optarg == "fmc") { + return MBQI_FMC; + } else if(optarg == "interval") { + return MBQI_INTERVAL; + } else if(optarg == "help") { + puts(mbqiModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --mbqi: `") + + optarg + "'. Try --mbqi help."); + } +} + +inline void checkMbqiMode(std::string option, MbqiMode mode, SmtEngine* smt) throw(OptionException) { + +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/qinterval_builder.cpp b/src/theory/quantifiers/qinterval_builder.cpp new file mode 100755 index 000000000..ce85cecc0 --- /dev/null +++ b/src/theory/quantifiers/qinterval_builder.cpp @@ -0,0 +1,1111 @@ +/********************* */
+/*! \file qinterval_builder.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of qinterval builder
+ **/
+
+
+#include "theory/quantifiers/qinterval_builder.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+//lower bound is exclusive
+//upper bound is inclusive
+
+struct QIntSort
+{
+ FirstOrderModelQInt * m;
+ bool operator() (Node i, Node j) {
+ return m->isLessThan( i, j );
+ }
+};
+
+void QIntDef::init_vec( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u ) {
+ for( unsigned i=0; i<m->getOrderedNumVars( q ); i++ ){
+ l.push_back( Node::null() );
+ u.push_back( m->getMaximum( m->getOrderedVarType( q, i ) ) );
+ }
+}
+
+void QIntDef::debugPrint( const char * c, FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u )
+{
+ Trace(c) << "( ";
+ for( unsigned i=0; i<l.size(); i++ ){
+ if( i>0 ) Trace(c) << ", ";
+ //Trace(c) << l[i] << "..." << u[i];
+ int lindex = l[i].isNull() ? 0 : m->getRepId( l[i] ) + 1;
+ int uindex = m->getRepId( u[i] );
+ Trace(c) << lindex << "..." << uindex;
+ }
+ Trace(c) << " )";
+}
+
+
+int QIntDef::getEvIndex( FirstOrderModelQInt * m, Node n, bool exc ) {
+ if( n.isNull() ){
+ Assert( exc );
+ return 0;
+ }else{
+ int min = 0;
+ int max = (int)(d_def_order.size()-1);
+ while( min!=max ){
+ int index = (min+max)/2;
+ Assert( index>=0 && index<(int)d_def_order.size() );
+ if( n==d_def_order[index] ){
+ max = index;
+ min = index;
+ }else if( m->isLessThan( n, d_def_order[index] ) ){
+ max = index;
+ }else{
+ min = index+1;
+ }
+ }
+ if( n==d_def_order[min] && exc ){
+ min++;
+ }
+ Assert( min>=0 && min<(int)d_def_order.size() );
+ if( ( min!=0 && !m->isLessThan( d_def_order[min-1], n ) && ( !exc || d_def_order[min-1]!=n ) ) ||
+ ( ( exc || d_def_order[min]!=n ) && !m->isLessThan( n, d_def_order[min] ) ) ){
+ Debug("qint-error") << "ERR size : " << d_def_order.size() << ", exc : " << exc << std::endl;
+ for( unsigned i=0; i<d_def_order.size(); i++ ){
+ Debug("qint-error") << "ERR ch #" << i << " : " << d_def_order[i];
+ Debug("qint-error") << " " << m->getRepId( d_def_order[i] ) << std::endl;
+ }
+ Debug("qint-error") << " : " << n << " " << min << " " << m->getRepId( n ) << std::endl;
+ }
+
+ Assert( min==0 || m->isLessThan( d_def_order[min-1], n ) || ( exc && d_def_order[min-1]==n ) );
+ Assert( ( !exc && n==d_def_order[min] ) || m->isLessThan( n, d_def_order[min] ) );
+ return min;
+ }
+}
+
+void QIntDef::addEntry( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,
+ Node v, unsigned depth ) {
+ if( depth==0 ){
+ Trace("qint-compose-debug") << "Add entry ";
+ debugPrint( "qint-compose-debug", m, q, l, u );
+ Trace("qint-compose-debug") << " -> " << v << "..." << std::endl;
+ }
+ //Assert( false );
+ if( depth==u.size() ){
+ Assert( d_def_order.empty() );
+ Assert( v.isNull() || v.isConst() || ( v.getType().isSort() && m->getRepId( v )!=-1 ) );
+ d_def_order.push_back( v );
+ }else{
+ /*
+ if( !d_def_order.empty() &&
+ ( l[depth].isNull() || m->isLessThan( l[depth], d_def_order[d_def_order.size()-1] ) ) ){
+ int startEvIndex = getEvIndex( m, l[depth], true );
+ int endEvIndex;
+ if( m->isLessThan( u[depth], d_def_order[d_def_order.size()-1] ) ){
+ endEvIndex = getEvIndex( m, u[depth] );
+ }else{
+ endEvIndex = d_def_order.size()-1;
+ }
+ Trace("qint-compose-debug2") << this << " adding for bounds " << l[depth] << "..." << u[depth] << std::endl;
+ for( int i=startEvIndex; i<=endEvIndex; i++ ){
+ Trace("qint-compose-debug2") << this << " add entry " << d_def_order[i] << std::endl;
+ d_def[d_def_order[i]].addEntry( m, q, l, u, v, depth+1 );
+ }
+ }
+ if( !d_def_order.empty() &&
+ d_def.find(u[depth])==d_def.end() &&
+ !m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){
+ Trace("qint-compose-debug2") << "Bad : depth : " << depth << std::endl;
+ }
+ Assert( d_def_order.empty() ||
+ d_def.find(u[depth])!=d_def.end() ||
+ m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) );
+
+ if( d_def_order.empty() || m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){
+ Trace("qint-compose-debug2") << this << " add entry new : " << u[depth] << std::endl;
+ d_def_order.push_back( u[depth] );
+ d_def[u[depth]].addEntry( m, q, l, u, v, depth+1 );
+ }
+ */
+ //%%%%%%
+ bool success = true;
+ int nnum = m->getVarOrder( q )->getNextNum( depth );
+ Node pl;
+ Node pu;
+ if( nnum!=-1 ){
+ Trace("qint-compose-debug2") << "...adding entry #" << depth << " is #" << nnum << std::endl;
+ //Assert( l[nnum].isNull() || l[nnum]==l[depth] || m->isLessThan( l[nnum], l[depth] ) );
+ //Assert( u[nnum]==u[depth] || m->isLessThan( u[depth], u[nnum] ) );
+ pl = l[nnum];
+ pu = u[nnum];
+ if( !m->doMeet( l[nnum], u[nnum], l[depth], u[depth], l[nnum], u[nnum] ) ){
+ success = false;
+ }
+ }
+ //%%%%%%
+ if( success ){
+ Node r = u[depth];
+ if( d_def.find( r )!=d_def.end() ){
+ d_def[r].addEntry( m, q, l, u, v, depth+1 );
+ }else{
+ if( !d_def_order.empty() &&
+ !m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){
+ Trace("qint-compose-debug2") << "Bad : depth : " << depth << " ";
+ Trace("qint-compose-debug2") << d_def_order[d_def_order.size()-1] << " " << u[depth] << std::endl;
+ }
+ Assert( d_def_order.empty() || m->isLessThan( d_def_order[d_def_order.size()-1], r ) );
+ d_def_order.push_back( r );
+ d_def[r].addEntry( m, q, l, u, v, depth+1 );
+ }
+ }
+ if( nnum!=-1 ){
+ l[nnum] = pl;
+ u[nnum] = pu;
+ }
+ }
+}
+
+Node QIntDef::simplify_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
+ unsigned depth ) {
+ if( d_def.empty() ){
+ if( d_def_order.size()!=0 ){
+ Debug("qint-error") << "Simplify, size = " << d_def_order.size() << std::endl;
+ }
+ Assert( d_def_order.size()==1 );
+ return d_def_order[0];
+ }else{
+ Assert( !d_def_order.empty() );
+ std::vector< Node > newDefs;
+ Node curr;
+ for( unsigned i=0; i<d_def_order.size(); i++ ){
+ Node n = d_def[d_def_order[i]].simplify_r( m, q, il, iu, depth+1 );
+ if( i>0 ){
+ if( n==curr && !n.isNull() ){
+ d_def.erase( d_def_order[i-1] );
+ }else{
+ newDefs.push_back( d_def_order[i-1] );
+ }
+ }
+ curr = n;
+ }
+ newDefs.push_back( d_def_order[d_def_order.size()-1] );
+ d_def_order.clear();
+ d_def_order.insert( d_def_order.end(), newDefs.begin(), newDefs.end() );
+ return d_def_order.size()==1 ? curr : Node::null();
+ }
+}
+
+Node QIntDef::simplify( FirstOrderModelQInt * m, Node q ) {
+ std::vector< Node > l;
+ std::vector< Node > u;
+ if( !q.isNull() ){
+ //init_vec( m, q, l, u );
+ }
+ return simplify_r( m, q, l, u, 0 );
+}
+
+bool QIntDef::isTotal_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,
+ unsigned depth ) {
+ if( d_def_order.empty() ){
+ return false;
+ }else if( d_def.empty() ){
+ return true;
+ }else{
+ //get the current maximum
+ Node mx;
+ if( !q.isNull() ){
+ int pnum = m->getVarOrder( q )->getPrevNum( depth );
+ if( pnum!=-1 ){
+ mx = u[pnum];
+ }
+ }
+ if( mx.isNull() ){
+ mx = m->getMaximum( d_def_order[d_def_order.size()-1].getType() );
+ }
+ //if not current maximum
+ if( d_def_order[d_def_order.size()-1]!=mx ){
+ return false;
+ }else{
+ Node pu = u[depth];
+ for( unsigned i=0; i<d_def_order.size(); i++ ){
+ u[depth] = d_def_order[i];
+ if( !d_def[d_def_order[i]].isTotal_r( m, q, l, u, depth+1 ) ){
+ return false;
+ }
+ }
+ u[depth] = pu;
+ return true;
+ }
+ }
+}
+
+bool QIntDef::isTotal( FirstOrderModelQInt * m, Node q ) {
+ std::vector< Node > l;
+ std::vector< Node > u;
+ if( !q.isNull() ){
+ init_vec( m, q, l, u );
+ }
+ return isTotal_r( m, q, l, u, 0 );
+}
+
+void QIntDef::construct_compose_r( FirstOrderModelQInt * m, Node q,
+ std::vector< Node >& l, std::vector< Node >& u,
+ Node n, QIntDef * f,
+ std::vector< Node >& args,
+ std::map< unsigned, QIntDef >& children,
+ std::map< unsigned, Node >& bchildren,
+ QIntVarNumIndex& vindex, unsigned depth ) {
+ //check for short circuit
+ if( !f ){
+ if( !args.empty() ){
+ if( ( n.getKind()==OR && args[args.size()-1]==m->d_true ) ||
+ ( n.getKind()==AND && args[args.size()-1]==m->d_false ) ){
+ addEntry( m, q, l, u, args[args.size()-1] );
+ return;
+ }
+ }
+ }
+
+ for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << " "; }
+ Trace("qint-compose") << (f ? "U" : "I" ) << "C( ";
+ for( unsigned i=0; i<l.size(); i++ ){
+ if( i>0 ) Trace("qint-compose") << ", ";
+ //Trace("qint-compose") << l[i] << "..." << u[i];
+ int lindex = l[i].isNull() ? 0 : m->getRepId( l[i] ) + 1;
+ int uindex = m->getRepId( u[i] );
+ Trace( "qint-compose" ) << lindex << "..." << uindex;
+ }
+ Trace("qint-compose") << " )...";
+
+ //finished?
+ if( ( f && f->d_def.empty() ) || args.size()==n.getNumChildren() ){
+ if( f ){
+ Assert( f->d_def_order.size()==1 );
+ Trace("qint-compose") << "UVALUE(" << f->d_def_order[0] << ")" << std::endl;
+ addEntry( m, q, l, u, f->d_def_order[0] );
+ }else{
+ Node nn;
+ bool nnSet = false;
+ for( unsigned i=0; i<args.size(); i++ ){
+ if( args[i].isNull() ){
+ nnSet = true;
+ break;
+ }
+ }
+ if( !nnSet ){
+ if( n.getKind()==EQUAL ){
+ nn = NodeManager::currentNM()->mkConst( args[0]==args[1] );
+ }else{
+ //apply the operator to args
+ nn = NodeManager::currentNM()->mkNode( n.getKind(), args );
+ nn = Rewriter::rewrite( nn );
+ }
+ }
+ Trace("qint-compose") << "IVALUE(" << nn << ")" << std::endl;
+ addEntry( m, q, l, u, nn );
+ Trace("qint-compose-debug2") << "...added entry." << std::endl;
+ }
+ }else{
+ //if a non-simple child
+ if( children.find( depth )!=children.end() ){
+ //***************************
+ Trace("qint-compose") << "compound child, recurse" << std::endl;
+ std::vector< int > currIndex;
+ std::vector< int > endIndex;
+ std::vector< Node > prevL;
+ std::vector< Node > prevU;
+ std::vector< QIntDef * > visited;
+ do{
+ Assert( currIndex.size()==visited.size() );
+
+ //populate the vectors
+ while( visited.size()<m->getOrderedNumVars( q ) ){
+ unsigned i = visited.size();
+ QIntDef * qq = visited.empty() ? &children[depth] : visited[i-1]->getChild( currIndex[i-1] );
+ visited.push_back( qq );
+ Node qq_mx = qq->getMaximum();
+ Trace("qint-compose-debug2") << "...Get ev indices " << i << " " << l[i] << " " << u[i] << std::endl;
+ currIndex.push_back( qq->getEvIndex( m, l[i], true ) );
+ Trace("qint-compose-debug2") << "...Done get curr index " << currIndex[currIndex.size()-1] << std::endl;
+ if( m->isLessThan( qq_mx, u[i] ) ){
+ endIndex.push_back( qq->getNumChildren()-1 );
+ }else{
+ endIndex.push_back( qq->getEvIndex( m, u[i] ) );
+ }
+ Trace("qint-compose-debug2") << "...Done get end index " << endIndex[endIndex.size()-1] << std::endl;
+ prevL.push_back( l[i] );
+ prevU.push_back( u[i] );
+ if( !m->doMeet( prevL[i], prevU[i],
+ qq->getLower( currIndex[i] ), qq->getUpper( currIndex[i] ), l[i], u[i] ) ){
+ Assert( false );
+ }
+ }
+ for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << " "; }
+ for( unsigned i=0; i<currIndex.size(); i++ ){
+ Trace("qint-compose") << "[" << currIndex[i] << "/" << endIndex[i] << "]";
+ }
+ Trace("qint-compose") << std::endl;
+ //consider the current
+ int activeIndex = visited.size()-1;
+ QIntDef * qa = visited.empty() ? &children[depth] : visited[activeIndex]->getChild( currIndex[activeIndex] );
+ if( f ){
+ int fIndex = f->getEvIndex( m, qa->getValue() );
+ construct_compose_r( m, q, l, u, n, f->getChild( fIndex ), args, children, bchildren, vindex, depth+1 );
+ }else{
+ args.push_back( qa->getValue() );
+ construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, depth+1 );
+ args.pop_back();
+ }
+
+ //increment the index (if possible)
+ while( activeIndex>=0 && currIndex[activeIndex]==endIndex[activeIndex] ){
+ currIndex.pop_back();
+ endIndex.pop_back();
+ l[activeIndex] = prevL[activeIndex];
+ u[activeIndex] = prevU[activeIndex];
+ prevL.pop_back();
+ prevU.pop_back();
+ visited.pop_back();
+ activeIndex--;
+ }
+ if( activeIndex>=0 ){
+ for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << " "; }
+ Trace("qint-compose-debug") << "Increment at " << activeIndex << std::endl;
+ currIndex[activeIndex]++;
+ if( !m->doMeet( prevL[activeIndex], prevU[activeIndex],
+ visited[activeIndex]->getLower( currIndex[activeIndex] ),
+ visited[activeIndex]->getUpper( currIndex[activeIndex] ),
+ l[activeIndex], u[activeIndex] ) ){
+ Assert( false );
+ }
+ }
+ }while( !visited.empty() );
+ //***************************
+ }else{
+ Assert( bchildren.find( depth )!=bchildren.end() );
+ Node v = bchildren[depth];
+ if( f ){
+ if( v.getKind()==BOUND_VARIABLE ){
+ int vn = vindex.d_var_num[depth];
+ Trace("qint-compose") << "variable #" << vn << ", recurse" << std::endl;
+ //int vn = m->getOrderedVarOccurId( q, n, depth );
+ Trace("qint-compose-debug") << "-process " << v << ", which is var #" << vn << std::endl;
+ Node lprev = l[vn];
+ Node uprev = u[vn];
+ //restrict to last variable in order
+ int pnum = m->getVarOrder( q )->getPrevNum( vn );
+ if( pnum!=-1 ){
+ Trace("qint-compose-debug") << "-restrict to var #" << pnum << " " << l[pnum] << " " << u[pnum] << std::endl;
+ l[vn] = l[pnum];
+ u[vn] = u[pnum];
+ }
+ int startIndex = f->getEvIndex( m, l[vn], true );
+ int endIndex = f->getEvIndex( m, u[vn] );
+ Trace("qint-compose-debug") << "--will process " << startIndex << " " << endIndex << std::endl;
+ for( int i=startIndex; i<=endIndex; i++ ){
+ if( m->doMeet( lprev, uprev, f->getLower( i ), f->getUpper( i ), l[vn], u[vn] ) ){
+ construct_compose_r( m, q, l, u, n, f->getChild( i ), args, children, bchildren, vindex, depth+1 );
+ }else{
+ Assert( false );
+ }
+ }
+ l[vn] = lprev;
+ u[vn] = uprev;
+ }else{
+ Trace("qint-compose") << "value, recurse" << std::endl;
+ //simple
+ int ei = f->getEvIndex( m, v );
+ construct_compose_r( m, q, l, u, n, f->getChild( ei ), args, children, bchildren, vindex, depth+1 );
+ }
+ }else{
+ Trace("qint-compose") << "value, recurse" << std::endl;
+ args.push_back( v );
+ construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, depth+1 );
+ args.pop_back();
+ }
+ }
+ }
+}
+
+
+void QIntDef::construct_enum_r( FirstOrderModelQInt * m, Node q, unsigned vn, unsigned depth, Node v ) {
+ if( depth==m->getOrderedNumVars( q ) ){
+ Assert( !v.isNull() );
+ d_def_order.push_back( v );
+ }else{
+ TypeNode tn = m->getOrderedVarType( q, depth );
+ //int vnum = m->getVarOrder( q )->getVar( depth )==
+ if( depth==vn ){
+ for( unsigned i=0; i<m->d_rep_set.d_type_reps[tn].size(); i++ ){
+ Node vv = m->d_rep_set.d_type_reps[tn][i];
+ d_def_order.push_back( vv );
+ d_def[vv].construct_enum_r( m, q, vn, depth+1, vv );
+ }
+ }else if( m->getVarOrder( q )->getVar( depth )==m->getVarOrder( q )->getVar( vn ) && depth>vn ){
+ d_def_order.push_back( v );
+ d_def[v].construct_enum_r( m, q, vn, depth+1, v );
+ }else{
+ Node mx = m->getMaximum( tn );
+ d_def_order.push_back( mx );
+ d_def[mx].construct_enum_r( m, q, vn, depth+1, v );
+ }
+ }
+}
+
+bool QIntDef::construct_enum( FirstOrderModelQInt * m, Node q, unsigned vn ) {
+ TypeNode tn = m->getOrderedVarType( q, vn );
+ if( tn.isSort() ){
+ construct_enum_r( m, q, vn, 0, Node::null() );
+ return true;
+ }else{
+ return false;
+ }
+}
+
+bool QIntDef::construct_compose( FirstOrderModelQInt * m, Node q, Node n, QIntDef * f,
+ std::map< unsigned, QIntDef >& children,
+ std::map< unsigned, Node >& bchildren, int varChCount,
+ QIntVarNumIndex& vindex ) {
+ Trace("qint-compose") << "Do " << (f ? "uninterpreted" : "interpreted");
+ Trace("qint-compose") << " compose, var count = " << varChCount << "..." << std::endl;
+ std::vector< Node > l;
+ std::vector< Node > u;
+ init_vec( m, q, l, u );
+ if( varChCount==0 || f ){
+ //standard (no variable child) interpreted compose, or uninterpreted compose
+ std::vector< Node > args;
+ construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, 0 );
+ }else{
+ //special cases
+ bool success = false;
+ int varIndex = ( bchildren.find( 0 )!=bchildren.end() && bchildren[0].getKind()==BOUND_VARIABLE ) ? 0 : 1;
+ if( varChCount>1 ){
+ if( n.getKind()==EQUAL ){
+ //make it an enumeration
+ unsigned vn = vindex.d_var_num[0];
+ if( children[0].construct_enum( m, q, vn ) ){
+ bchildren.erase( 0 );
+ varIndex = 1;
+ success = true;
+ }
+ }
+ }else{
+ success = n.getKind()==EQUAL;
+ }
+ if( success ){
+ int oIndex = varIndex==0 ? 1 : 0;
+ Node v = bchildren[varIndex];
+ unsigned vn = vindex.d_var_num[varIndex];
+ if( children.find( oIndex )==children.end() ){
+ Assert( bchildren.find( oIndex )!=bchildren.end() );
+ Node at = bchildren[oIndex];
+ Trace("qint-icompose") << "Basic child, " << at << " with var " << v << std::endl;
+ Node prev = m->getPrev( bchildren[oIndex].getType(), bchildren[oIndex] );
+ Node above = u[vn];
+ if( !prev.isNull() ){
+ u[vn] = prev;
+ addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( false ) );
+ }
+ l[vn] = prev;
+ u[vn] = at;
+ addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( true ) );
+ if( at!=above ){
+ l[vn] = at;
+ u[vn] = above;
+ addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( false ) );
+ }
+ }else{
+ QIntDef * qid = &children[oIndex];
+ qid->debugPrint("qint-icompose", m, q );
+ Trace("qint-icompose") << " against variable..." << v << ", which is var #" << vn << std::endl;
+
+ TypeNode tn = v.getType();
+ QIntDefIter qdi( m, q, qid );
+ while( !qdi.isFinished() ){
+ std::vector< Node > us;
+ qdi.getUppers( us );
+ std::vector< Node > ls;
+ qdi.getLowers( ls );
+ qdi.debugPrint( "qint-icompose" );
+
+ Node n_below = ls[vn];
+ Node n_prev = m->getPrev( tn, qdi.getValue() );
+ Node n_at = qdi.getValue();
+ Node n_above = us[vn];
+ Trace("qint-icompose") << n_below << " < " << n_prev << " < " << n_at << " < " << n_above << std::endl;
+ if( n.getKind()==EQUAL ){
+ bool atLtAbove = m->isLessThan( n_at, n_above );
+ Node currL = n_below;
+ if( n_at==n_above || atLtAbove ){
+ //add for value (at-1)
+ if( !n_prev.isNull() && ( n_below.isNull() || m->isLessThan( n_below, n_prev ) ) ){
+ ls[vn] = currL;
+ us[vn] = n_prev;
+ currL = n_prev;
+ Trace("qint-icompose") << "-add entry(-) at " << ls[vn] << "..." << us[vn] << std::endl;
+ addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( false ) );
+ }
+ //add for value (at)
+ if( ( n_below.isNull() || m->isLessThan( n_below, n_at ) ) && atLtAbove ){
+ ls[vn] = currL;
+ us[vn] = n_at;
+ currL = n_at;
+ Trace("qint-icompose") << "-add entry(=) at " << ls[vn] << "..." << us[vn] << std::endl;
+ addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( true ) );
+ }
+ }
+ ls[vn] = currL;
+ us[vn] = n_above;
+ Trace("qint-icompose") << "-add entry(+) at " << ls[vn] << "..." << us[vn] << std::endl;
+ addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( n_at==n_above ) );
+ }else{
+ return false;
+ }
+ qdi.increment();
+
+ Trace("qint-icompose-debug") << "Now : " << std::endl;
+ debugPrint("qint-icompose-debug", m, q );
+ Trace("qint-icompose-debug") << std::endl;
+ }
+ }
+
+ Trace("qint-icompose") << "Result : " << std::endl;
+ debugPrint("qint-icompose", m, q );
+ Trace("qint-icompose") << std::endl;
+
+ }else{
+ return false;
+ }
+ }
+ Trace("qint-compose") << "Done i-compose" << std::endl;
+ return true;
+}
+
+
+void QIntDef::construct( FirstOrderModelQInt * m, std::vector< Node >& fapps, unsigned depth ) {
+ d_def.clear();
+ d_def_order.clear();
+ Assert( !fapps.empty() );
+ if( depth==fapps[0].getNumChildren() ){
+ //get representative in model for this term
+ Assert( fapps.size()>=1 );
+ Node r = m->getUsedRepresentative( fapps[0] );
+ d_def_order.push_back( r );
+ }else{
+ std::map< Node, std::vector< Node > > fapp_child;
+ //partition based on evaluations of fapps[1][depth]....fapps[n][depth]
+ for( unsigned i=0; i<fapps.size(); i++ ){
+ Node r = m->getUsedRepresentative( fapps[i][depth] );
+ fapp_child[r].push_back( fapps[i] );
+ }
+ //sort by QIntSort
+ for( std::map< Node, std::vector< Node > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){
+ d_def_order.push_back( it->first );
+ }
+ QIntSort qis;
+ qis.m = m;
+ std::sort( d_def_order.begin(), d_def_order.end(), qis );
+ //construct children
+ for( unsigned i=0; i<d_def_order.size(); i++ ){
+ Node n = d_def_order[i];
+ if( i==d_def_order.size()-1 ){
+ d_def_order[i] = m->getMaximum( d_def_order[i].getType() );
+ }
+ Debug("qint-model-debug2") << "Construct for " << n << ", terms = " << fapp_child[n].size() << std::endl;
+ d_def[d_def_order[i]].construct( m, fapp_child[n], depth+1 );
+ }
+ }
+}
+
+Node QIntDef::getFunctionValue( FirstOrderModelQInt * m, std::vector< Node >& vars, unsigned depth ) {
+ if( d_def.empty() ){
+ Assert( d_def_order.size()==1 );
+ //must convert to actual domain constant
+ if( d_def_order[0].getType().isSort() ){
+ return m->d_rep_set.d_type_reps[ d_def_order[0].getType() ][ m->getRepId( d_def_order[0] ) ];
+ }else{
+ return m->getUsedRepresentative( d_def_order[0] );
+ }
+ }else{
+ TypeNode tn = vars[depth].getType();
+ Node curr;
+ int rep_id = m->d_rep_set.getNumRepresentatives( tn );
+ for( int i=(int)(d_def_order.size()-1); i>=0; i-- ){
+ int curr_rep_id = i==0 ? 0 : m->getRepId( d_def_order[i-1] )+1;
+ Node ccurr = d_def[d_def_order[i]].getFunctionValue( m, vars, depth+1 );
+ if( curr.isNull() ){
+ curr = ccurr;
+ }else{
+ std::vector< Node > c;
+ Assert( curr_rep_id<rep_id );
+ for( int j=curr_rep_id; j<rep_id; j++ ){
+ c.push_back( vars[depth].eqNode( m->d_rep_set.d_type_reps[tn][j] ) );
+ }
+ Node cond = c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( OR, c );
+ curr = NodeManager::currentNM()->mkNode( ITE, cond, ccurr, curr );
+ }
+ rep_id = curr_rep_id;
+ }
+ return curr;
+ }
+}
+
+Node QIntDef::evaluate_r( FirstOrderModelQInt * m, std::vector< Node >& reps, unsigned depth ) {
+ if( depth==reps.size() ){
+ Assert( d_def_order.size()==1 );
+ return d_def_order[0];
+ }else{
+ if( d_def.find( reps[depth] )!=d_def.end() ){
+ return d_def[reps[depth]].evaluate_r( m, reps, depth+1 );
+ }else{
+ int ei = getEvIndex( m, reps[depth] );
+ return d_def[d_def_order[ei]].evaluate_r( m, reps, depth+1 );
+ }
+ }
+}
+Node QIntDef::evaluate_n_r( FirstOrderModelQInt * m, Node n, unsigned depth ) {
+ if( depth==n.getNumChildren() ){
+ Assert( d_def_order.size()==1 );
+ return d_def_order[0];
+ }else{
+ Node r = m->getUsedRepresentative( n[depth] );
+ if( d_def.find( r )!=d_def.end() ){
+ return d_def[r].evaluate_n_r( m, n, depth+1 );
+ }else{
+ int ei = getEvIndex( m, r );
+ return d_def[d_def_order[ei]].evaluate_n_r( m, n, depth+1 );
+ }
+ }
+}
+
+
+
+QIntDef * QIntDef::getChild( unsigned i ) {
+ Assert( i<d_def_order.size() );
+ Assert( d_def.find( d_def_order[i] )!=d_def.end() );
+ return &d_def[ d_def_order[i] ];
+}
+
+void QIntDef::debugPrint( const char * c, FirstOrderModelQInt * m, Node q, int t ) {
+ /*
+ for( unsigned i=0; i<d_def_order.size(); i++ ){
+ for( int j=0; j<t; j++ ) { Trace(c) << " "; }
+ //Trace(c) << this << " ";
+ Trace(c) << d_def_order[i] << " : " << std::endl;
+ if( d_def.find( d_def_order[i] )!=d_def.end() ){
+ d_def[d_def_order[i]].debugPrint( c, m, t+1 );
+ }
+ }
+ */
+ //if( t==0 ){
+ QIntDefIter qdi( m, q, this );
+ while( !qdi.isFinished() ){
+ qdi.debugPrint( c, t );
+ qdi.increment();
+ }
+ //}
+}
+
+
+QIntDefIter::QIntDefIter( FirstOrderModelQInt * m, Node q, QIntDef * qid ) : d_fm( m ), d_q( q ){
+ resetIndex( qid );
+}
+
+void QIntDefIter::debugPrint( const char * c, int t ) {
+ //Trace( c ) << getSize() << " " << d_index_visited.size() << " ";
+ for( int j=0; j<t; j++ ) { Trace(c) << " "; }
+ std::vector< Node > l;
+ std::vector< Node > u;
+ getLowers( l );
+ getUppers( u );
+ QIntDef::debugPrint( c, d_fm, d_q, l, u );
+ Trace( c ) << " -> " << getValue() << std::endl;
+}
+
+void QIntDefIter::resetIndex( QIntDef * qid ){
+ //std::cout << "check : " << qid << " " << qid->d_def_order.size() << " " << qid->d_def.size() << std::endl;
+ if( !qid->d_def.empty() ){
+ //std::cout << "add to visited " << qid << std::endl;
+ d_index.push_back( 0 );
+ d_index_visited.push_back( qid );
+ resetIndex( qid->getChild( 0 ) );
+ }
+}
+
+bool QIntDefIter::increment( int index ) {
+ if( !isFinished() ){
+ index = index==-1 ? (int)(d_index.size()-1) : index;
+ while( (int)(d_index.size()-1)>index ){
+ //std::cout << "remove from visit 1 " << std::endl;
+ d_index.pop_back();
+ d_index_visited.pop_back();
+ }
+ while( index>=0 && d_index[index]>=(int)(d_index_visited[index]->d_def_order.size()-1) ){
+ //std::cout << "remove from visit " << d_index_visited[ d_index_visited.size()-1 ] << std::endl;
+ d_index.pop_back();
+ d_index_visited.pop_back();
+ index--;
+ }
+ if( index>=0 ){
+ //std::cout << "increment at index = " << index << std::endl;
+ d_index[index]++;
+ resetIndex( d_index_visited[index]->getChild( d_index[index] ) );
+ return true;
+ }else{
+ d_index.clear();
+ return false;
+ }
+ }else{
+ return false;
+ }
+}
+
+Node QIntDefIter::getLower( int index ) {
+ if( d_index[index]==0 && !d_q.isNull() ){
+ int pnum = d_fm->getVarOrder( d_q )->getPrevNum( index );
+ if( pnum!=-1 ){
+ return getLower( pnum );
+ }
+ }
+ return d_index_visited[index]->getLower( d_index[index] );
+}
+
+Node QIntDefIter::getUpper( int index ) {
+ return d_index_visited[index]->getUpper( d_index[index] );
+}
+
+void QIntDefIter::getLowers( std::vector< Node >& reps ) {
+ for( unsigned i=0; i<getSize(); i++ ){
+ bool added = false;
+ if( d_index[i]==0 && !d_q.isNull() ){
+ int pnum = d_fm->getVarOrder( d_q )->getPrevNum( i );
+ if( pnum!=-1 ){
+ added = true;
+ reps.push_back( reps[pnum] );
+ }
+ }
+ if( !added ){
+ reps.push_back( getLower( i ) );
+ }
+ }
+}
+
+void QIntDefIter::getUppers( std::vector< Node >& reps ) {
+ for( unsigned i=0; i<getSize(); i++ ){
+ reps.push_back( getUpper( i ) );
+ }
+}
+
+Node QIntDefIter::getValue() {
+ return d_index_visited[ d_index_visited.size()-1 ]->getChild( d_index[d_index.size()-1] )->getValue();
+}
+
+
+//------------------------variable ordering----------------------------
+
+QuantVarOrder::QuantVarOrder( Node q ) : d_q( q ) {
+ d_var_count = 0;
+ initialize( q[1], 0, d_var_occur );
+}
+
+int QuantVarOrder::initialize( Node n, int minVarIndex, QIntVarNumIndex& vindex ) {
+ if( n.getKind()!=FORALL ){
+ //std::vector< Node > vars;
+ //std::vector< int > args;
+ int procVarOn = n.getKind()==APPLY_UF ? 0 : 1;
+ for( int r=0; r<=procVarOn; r++ ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( n[i].getKind()==BOUND_VARIABLE && r==procVarOn ){
+ int occ_index = -1;
+ for( unsigned j=0; j<d_var_to_num[n[i]].size(); j++ ){
+ if( d_var_to_num[n[i]][j]>=minVarIndex ){
+ occ_index = d_var_to_num[n[i]][j];
+ }
+ }
+ if( occ_index==-1 ){
+ //need to assign new
+ d_num_to_var[d_var_count] = n[i];
+ if( !d_var_to_num[n[i]].empty() ){
+ int v = d_var_to_num[n[i]][ d_var_to_num[n[i]].size()-1 ];
+ d_num_to_prev_num[ d_var_count ] = v;
+ d_num_to_next_num[ v ] = d_var_count;
+ }
+ d_var_num_index[ d_var_count ] = d_var_to_num[n[i]].size();
+ d_var_to_num[n[i]].push_back( d_var_count );
+ occ_index = d_var_count;
+ d_var_count++;
+ }
+ vindex.d_var_num[i] = occ_index;
+ minVarIndex = occ_index;
+ }else if( r==0 ){
+ minVarIndex = initialize( n[i], minVarIndex, vindex.d_var_index[i] );
+ }
+ }
+ }
+ }
+ return minVarIndex;
+}
+
+bool QuantVarOrder::getInstantiation( FirstOrderModelQInt * m, std::vector< Node >& l, std::vector< Node >& u,
+ std::vector< Node >& inst ) {
+ Debug("qint-var-order-debug2") << "Get for " << d_q << " " << l.size() << " " << u.size() << std::endl;
+ for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){
+ Debug("qint-var-order-debug2") << "Get for " << d_q[0][i] << " " << d_var_to_num[d_q[0][i]].size() << std::endl;
+ Node ll = Node::null();
+ Node uu = m->getMaximum( d_q[0][i].getType() );
+ for( unsigned j=0; j<d_var_to_num[d_q[0][i]].size(); j++ ){
+ Debug("qint-var-order-debug2") << "Go " << j << std::endl;
+ Node cl = ll;
+ Node cu = uu;
+ int index = d_var_to_num[d_q[0][i]][j];
+ Debug("qint-var-order-debug2") << "Do meet for " << index << "..." << std::endl;
+ Debug("qint-var-order-debug2") << l[index] << " " << u[index] << " " << cl << " " << cu << std::endl;
+ if( !m->doMeet( l[index], u[index], cl, cu, ll, uu ) ){
+ Debug("qint-var-order-debug2") << "FAILED" << std::endl;
+ return false;
+ }
+ Debug("qint-var-order-debug2") << "Result : " << ll << " " << uu << std::endl;
+ }
+ Debug("qint-var-order-debug2") << "Got " << uu << std::endl;
+ inst.push_back( uu );
+ }
+ return true;
+}
+
+void QuantVarOrder::debugPrint( const char * c ) {
+ Trace( c ) << "Variable order for " << d_q << " is : " << std::endl;
+ debugPrint( c, d_q[1], d_var_occur );
+ Trace( c ) << std::endl;
+ for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){
+ Trace( c ) << d_q[0][i] << " : ";
+ for( unsigned j=0; j<d_var_to_num[d_q[0][i]].size(); j++ ){
+ Trace( c ) << d_var_to_num[d_q[0][i]][j] << " ";
+ }
+ Trace( c ) << std::endl;
+ }
+}
+
+void QuantVarOrder::debugPrint( const char * c, Node n, QIntVarNumIndex& vindex ) {
+ if( n.getKind()==FORALL ){
+ Trace(c) << "NESTED_QUANT";
+ }else{
+ Trace(c) << n.getKind() << "(";
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( i>0 ) Trace( c ) << ",";
+ Trace( c ) << " ";
+ if( n[i].getKind()==BOUND_VARIABLE ){
+ Trace(c) << "VAR[" << vindex.d_var_num[i] << "]";
+ }else{
+ debugPrint( c, n[i], vindex.d_var_index[i] );
+ }
+ if( i==n.getNumChildren()-1 ) Trace( c ) << " ";
+ }
+ Trace(c) << ")";
+ }
+}
+
+QIntervalBuilder::QIntervalBuilder( context::Context* c, QuantifiersEngine* qe ) :
+QModelBuilder( c, qe ){
+ d_true = NodeManager::currentNM()->mkConst( true );
+}
+
+
+//------------------------model construction----------------------------
+
+void QIntervalBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
+ Trace("fmf-qint-debug") << "process build model " << fullModel << std::endl;
+ FirstOrderModel* f = (FirstOrderModel*)m;
+ FirstOrderModelQInt* fm = f->asFirstOrderModelQInt();
+ if( fullModel ){
+ Trace("qint-model") << "Construct model representation..." << std::endl;
+ //make function values
+ for( std::map<Node, QIntDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+ if( it->first.getType().getNumChildren()>1 ){
+ Trace("qint-model") << "Construct for " << it->first << "..." << std::endl;
+ m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" );
+ }
+ }
+ TheoryEngineModelBuilder::processBuildModel( m, fullModel );
+ //mark that the model has been set
+ fm->markModelSet();
+ //debug the model
+ debugModel( fm );
+ }else{
+ fm->initialize( d_considerAxioms );
+ //process representatives
+ fm->d_rep_id.clear();
+ fm->d_max.clear();
+ fm->d_min.clear();
+ Trace("qint-model") << std::endl << "Making representatives..." << std::endl;
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+ it != fm->d_rep_set.d_type_reps.end(); ++it ){
+ if( it->first.isSort() ){
+ if( it->second.empty() ){
+ std::cout << "Empty rep for " << it->first << std::endl;
+ exit(0);
+ }
+ Trace("qint-model") << "Representatives for " << it->first << " : " << std::endl;
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ Trace("qint-model") << i << " : " << it->second[i] << std::endl;
+ fm->d_rep_id[it->second[i]] = i;
+ }
+ fm->d_min[it->first] = it->second[0];
+ fm->d_max[it->first] = it->second[it->second.size()-1];
+ }else{
+ //TODO: enumerate?
+ }
+ }
+ Trace("qint-model") << std::endl << "Making function definitions..." << std::endl;
+ //construct the models for functions
+ for( std::map<Node, QIntDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+ Node f = it->first;
+ Trace("qint-model-debug") << "Building Model for " << f << std::endl;
+ //reset the model
+ //get all (non-redundant) f-applications
+ std::vector< Node > fapps;
+ Trace("qint-model-debug") << "Initial terms: " << std::endl;
+ for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
+ Node n = fm->d_uf_terms[f][i];
+ if( !n.getAttribute(NoMatchAttribute()) ){
+ Trace("qint-model-debug") << " " << n << std::endl;
+ fapps.push_back( n );
+ }
+ }
+ if( fapps.empty() ){
+ //choose arbitrary value
+ Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);
+ Trace("qint-model-debug") << "Initial terms empty, add " << mbt << std::endl;
+ fapps.push_back( mbt );
+ }
+ //construct the interval model
+ it->second->construct( fm, fapps );
+ Trace("qint-model-debug") << "Definition for " << f << " : " << std::endl;
+ it->second->debugPrint("qint-model-debug", fm, Node::null() );
+
+ it->second->simplify( fm, Node::null() );
+ Trace("qint-model") << "(Simplified) definition for " << f << " : " << std::endl;
+ it->second->debugPrint("qint-model", fm, Node::null() );
+
+ if( Debug.isOn("qint-model-debug") ){
+ for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
+ Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );
+ Debug("qint-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;
+ Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );
+ }
+ }
+ }
+ }
+}
+
+
+//--------------------model checking---------------------------------------
+
+//do exhaustive instantiation
+bool QIntervalBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
+ Trace("qint-check") << "exhaustive instantiation " << q << " " << effort << std::endl;
+ if (effort==0) {
+
+ FirstOrderModelQInt * fmqint = fm->asFirstOrderModelQInt();
+ QIntDef qid;
+ doCheck( fmqint, q, qid, q[1], fmqint->d_var_order[q]->d_var_occur );
+ //now process entries
+ Trace("qint-inst") << "Interpretation for " << q << " is : " << std::endl;
+ qid.debugPrint( "qint-inst", fmqint, q );
+ Trace("qint-inst") << std::endl;
+ Debug("qint-check-debug2") << "Make iterator..." << std::endl;
+ QIntDefIter qdi( fmqint, q, &qid );
+ while( !qdi.isFinished() ){
+ if( qdi.getValue()!=d_true ){
+ Debug("qint-check-debug2") << "Set up vectors..." << std::endl;
+ std::vector< Node > l;
+ std::vector< Node > u;
+ std::vector< Node > inst;
+ qdi.getLowers( l );
+ qdi.getUppers( u );
+ Debug("qint-check-debug2") << "Get instantiation..." << std::endl;
+ if( fmqint->d_var_order[q]->getInstantiation( fmqint, l, u, inst ) ){
+ Trace("qint-inst") << "** Instantiate with ";
+ //just add the instance
+ InstMatch m;
+ for( unsigned j=0; j<inst.size(); j++) {
+ m.set( d_qe, q, j, inst[j] );
+ Trace("qint-inst") << inst[j] << " ";
+ }
+ Trace("qint-inst") << std::endl;
+ d_triedLemmas++;
+ if( d_qe->addInstantiation( q, m ) ){
+ Trace("qint-inst") << " ...added instantiation." << std::endl;
+ d_addedLemmas++;
+ }else{
+ Trace("qint-inst") << " ...duplicate instantiation" << std::endl;
+ //verify that instantiation is witness for current entry
+ if( Debug.isOn("qint-check-debug2") ){
+ Debug("qint-check-debug2") << "Check if : ";
+ std::vector< Node > exp_inst;
+ for( unsigned i=0; i<fmqint->getOrderedNumVars( q ); i++ ){
+ int index = fmqint->getOrderedVarNumToVarNum( q, i );
+ exp_inst.push_back( inst[ index ] );
+ Debug("qint-check-debug2") << inst[index] << " ";
+ }
+ Debug("qint-check-debug2") << " evaluates to " << qdi.getValue() << std::endl;
+ Assert( qid.evaluate( fmqint, exp_inst )==qdi.getValue() );
+ }
+ }
+ }else{
+ Trace("qint-inst") << "** Spurious instantiation." << std::endl;
+ }
+ }
+ qdi.increment();
+ }
+ }
+ return true;
+}
+
+bool QIntervalBuilder::doCheck( FirstOrderModelQInt * m, Node q, QIntDef & qid, Node n,
+ QIntVarNumIndex& vindex ) {
+ Assert( n.getKind()!=FORALL );
+ std::map< unsigned, QIntDef > children;
+ std::map< unsigned, Node > bchildren;
+ int varChCount = 0;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( n[i].getKind()==FORALL ){
+ bchildren[i] = Node::null();
+ }else if( n[i].getKind() == BOUND_VARIABLE ){
+ varChCount++;
+ bchildren[i] = n[i];
+ }else if( m->hasTerm( n[i] ) ){
+ bchildren[i] = m->getUsedRepresentative( n[i] );
+ }else{
+ if( !doCheck( m, q, children[i], n[i], vindex.d_var_index[i] ) ){
+ bchildren[i] = Node::null();
+ }
+ }
+ }
+ Trace("qint-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl;
+ if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){
+ Node op = n.getKind() == APPLY_UF ? n.getOperator() : n;
+ //uninterpreted compose
+ qid.construct_compose( m, q, n, m->d_models[op], children, bchildren, varChCount, vindex );
+ }else if( !qid.construct_compose( m, q, n, NULL, children, bchildren, varChCount, vindex ) ){
+ Trace("qint-check-debug") << "** Cannot produce definition for " << n << std::endl;
+ return false;
+ }
+ Trace("qint-check-debug2") << "Definition for " << n << " is : " << std::endl;
+ qid.debugPrint("qint-check-debug2", m, q);
+ qid.simplify( m, q );
+ Trace("qint-check-debug") << "(Simplified) Definition for " << n << " is : " << std::endl;
+ qid.debugPrint("qint-check-debug", m, q);
+ Trace("qint-check-debug") << std::endl;
+ Assert( qid.isTotal( m, q ) );
+ return true;
+}
diff --git a/src/theory/quantifiers/qinterval_builder.h b/src/theory/quantifiers/qinterval_builder.h new file mode 100755 index 000000000..8f48776cc --- /dev/null +++ b/src/theory/quantifiers/qinterval_builder.h @@ -0,0 +1,155 @@ +/********************* */
+/*! \file qinterval_builder.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief qinterval model class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef QINTERVAL_BUILDER
+#define QINTERVAL_BUILDER
+
+#include "theory/quantifiers/model_builder.h"
+#include "theory/quantifiers/first_order_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class FirstOrderModelQInt;
+
+class QIntVarNumIndex
+{
+public:
+ std::map< int, int > d_var_num;
+ std::map< int, QIntVarNumIndex > d_var_index;
+};
+
+class QIntDef
+{
+private:
+ Node evaluate_r( FirstOrderModelQInt * m, std::vector< Node >& reps, unsigned depth );
+ Node evaluate_n_r( FirstOrderModelQInt * m, Node n, unsigned depth );
+ void construct_compose_r( FirstOrderModelQInt * m, Node q,
+ std::vector< Node >& l, std::vector< Node >& u, Node n, QIntDef * f,
+ std::vector< Node >& args,
+ std::map< unsigned, QIntDef >& children,
+ std::map< unsigned, Node >& bchildren,
+ QIntVarNumIndex& vindex,
+ unsigned depth );
+
+ void construct_enum_r( FirstOrderModelQInt * m, Node q, unsigned vn, unsigned depth, Node v );
+ int getEvIndex( FirstOrderModelQInt * m, Node n, bool exc = false );
+ void addEntry( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,
+ Node v, unsigned depth = 0 );
+ Node simplify_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
+ unsigned depth );
+ bool isTotal_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
+ unsigned depth );
+public:
+ QIntDef(){}
+ std::map< Node, QIntDef > d_def;
+ std::vector< Node > d_def_order;
+
+ void construct( FirstOrderModelQInt * m, std::vector< Node >& fapps, unsigned depth = 0 );
+ bool construct_compose( FirstOrderModelQInt * m, Node q, Node n, QIntDef * f,
+ std::map< unsigned, QIntDef >& children,
+ std::map< unsigned, Node >& bchildren, int varChCount,
+ QIntVarNumIndex& vindex );
+ bool construct_enum( FirstOrderModelQInt * m, Node q, unsigned vn );
+
+ Node evaluate( FirstOrderModelQInt * m, std::vector< Node >& reps ) { return evaluate_r( m, reps, 0 ); }
+ Node evaluate_n( FirstOrderModelQInt * m, Node n ) { return evaluate_n_r( m, n, 0 ); }
+
+ void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, int t = 0 );
+ QIntDef * getChild( unsigned i );
+ Node getValue() { return d_def_order[0]; }
+ Node getLower( unsigned i ) { return i==0 ? Node::null() : d_def_order[i-1]; }
+ Node getUpper( unsigned i ) { return d_def_order[i]; }
+ Node getMaximum() { return d_def_order.empty() ? Node::null() : getUpper( d_def_order.size()-1 ); }
+ int getNumChildren() { return d_def_order.size(); }
+ bool isTotal( FirstOrderModelQInt * m, Node q );
+
+ Node simplify( FirstOrderModelQInt * m, Node q );
+ Node getFunctionValue( FirstOrderModelQInt * m, std::vector< Node >& vars, unsigned depth = 0 );
+
+ static void init_vec( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u );
+ static void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u );
+};
+
+class QIntDefIter {
+private:
+ FirstOrderModelQInt * d_fm;
+ Node d_q;
+ void resetIndex( QIntDef * qid );
+public:
+ QIntDefIter( FirstOrderModelQInt * m, Node q, QIntDef * qid );
+ void debugPrint( const char * c, int t = 0 );
+ std::vector< QIntDef * > d_index_visited;
+ std::vector< int > d_index;
+ bool isFinished() { return d_index.empty(); }
+ bool increment( int index = -1 );
+ unsigned getSize() { return d_index.size(); }
+ Node getLower( int index );
+ Node getUpper( int index );
+ void getLowers( std::vector< Node >& reps );
+ void getUppers( std::vector< Node >& reps );
+ Node getValue();
+};
+
+
+class QuantVarOrder
+{
+private:
+ int initialize( Node n, int minVarIndex, QIntVarNumIndex& vindex );
+ int d_var_count;
+ Node d_q;
+ void debugPrint( const char * c, Node n, QIntVarNumIndex& vindex );
+public:
+ QuantVarOrder( Node q );
+ std::map< int, Node > d_num_to_var;
+ std::map< int, int > d_num_to_prev_num;
+ std::map< int, int > d_num_to_next_num;
+ std::map< Node, std::vector< int > > d_var_to_num;
+ std::map< int, int > d_var_num_index;
+ //std::map< Node, std::map< int, int > > d_var_occur;
+ //int getVarNum( Node n, int arg ) { return d_var_occur[n][arg]; }
+ unsigned getNumVars() { return d_var_count; }
+ Node getVar( int i ) { return d_num_to_var[i]; }
+ int getPrevNum( int i ) { return d_num_to_prev_num.find( i )!=d_num_to_prev_num.end() ? d_num_to_prev_num[i] : -1; }
+ int getNextNum( int i ) { return d_num_to_next_num.find( i )!=d_num_to_next_num.end() ? d_num_to_next_num[i] : -1; }
+ int getVarNumIndex( int i ) { return d_var_num_index[i]; }
+ bool getInstantiation( FirstOrderModelQInt * m, std::vector< Node >& l, std::vector< Node >& u,
+ std::vector< Node >& inst );
+ void debugPrint( const char * c );
+ QIntVarNumIndex d_var_occur;
+};
+
+class QIntervalBuilder : public QModelBuilder
+{
+private:
+ Node d_true;
+ bool doCheck( FirstOrderModelQInt * m, Node q, QIntDef & qid, Node n,
+ QIntVarNumIndex& vindex );
+public:
+ QIntervalBuilder( context::Context* c, QuantifiersEngine* qe );
+ //process build model
+ void processBuildModel(TheoryModel* m, bool fullModel);
+ //do exhaustive instantiation
+ bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
+};
+
+
+}
+}
+}
+
+#endif
\ No newline at end of file diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index e18a4e0dc..6b1368be1 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -146,6 +146,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){ NoMatchAttribute nma; n.setAttribute(nma,true); + Debug("term-db-cong") << n << " is redundant." << std::endl; congruentCount++; }else{ nonCongruentCount++; @@ -173,6 +174,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ NoMatchAttribute nma; en.setAttribute(nma,true); + Debug("term-db-cong") << en << " is redundant." << std::endl; congruentCount++; }else{ nonCongruentCount++; @@ -222,10 +224,14 @@ Node TermDb::getModelBasisOpTerm( Node op ){ TypeNode t = op.getType(); std::vector< Node > children; children.push_back( op ); - for( size_t i=0; i<t.getNumChildren()-1; i++ ){ + for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){ children.push_back( getModelBasisTerm( t[i] ) ); } - d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + if( children.size()==1 ){ + d_model_basis_op_term[op] = op; + }else{ + d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + } } return d_model_basis_op_term[op]; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e9a69bd30..0388a2979 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -49,11 +49,14 @@ d_lemmas_produced_c(u){ d_eem = new EfficientEMatcher( this ); d_hasAddedLemma = false; + Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; //the model object - if( options::fmfFullModelCheck() || options::fmfBoundInt() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC || options::fmfBoundInt() ){ d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); + }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ + d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" ); }else{ - d_model = new quantifiers::FirstOrderModelIG( c, "FirstOrderModelIG" ); + d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" ); } //add quantifiers modules diff --git a/src/theory/theory.h b/src/theory/theory.h index fdd2d0518..43d35ac9d 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -254,6 +254,7 @@ protected: , d_sharedTerms(satContext) , d_out(&out) , d_valuation(valuation) + , d_proofEnabled(false) { StatisticsRegistry::registerStat(&d_computeCareGraphTime); } @@ -299,6 +300,12 @@ protected: void printFacts(std::ostream& os) const; void debugPrintFacts() const; + /** + * Whether proofs are enabled + * + */ + bool d_proofEnabled; + public: /** diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index cb44b42df..df1d2ebde 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -71,8 +71,8 @@ void EqualityEngine::init() { addTermInternal(d_false); d_trueId = getNodeId(d_true); - d_falseId = getNodeId(d_false); -} + d_falseId = getNodeId(d_false); +} EqualityEngine::~EqualityEngine() throw(AssertionException) { free(d_triggerDatabase); @@ -287,7 +287,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { d_isConstant[result] = t.isConst(); // If interpreted, set the number of non-interpreted children if (isInterpreted) { - // How many children are not constants yet + // How many children are not constants yet d_subtermsToEvaluate[result] = t.getNumChildren(); for (unsigned i = 0; i < t.getNumChildren(); ++ i) { if (isConstant(getNodeId(t[i]))) { @@ -316,11 +316,11 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) { d_newSetTags = Theory::setInsert(currentTheory, d_newSetTags); d_newSetTriggers[currentTheory] = tId; - } + } // Add it to the list for backtracking d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id)); d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1; - // Mark the the new set as a trigger + // Mark the the new set as a trigger d_nodeIndividualTrigger[tId] = newTriggerTermSet(); } @@ -333,7 +333,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { propagate(); Assert(hasTerm(t)); - + Debug("equality") << d_name << "::eq::addTermInternal(" << t << ") => " << result << std::endl; } @@ -419,12 +419,12 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; assertEqualityInternal(eq, d_false, reason); - propagate(); - + propagate(); + if (d_done) { return; } - + // If both have constant representatives, we don't notify anyone EqualityNodeId a = getNodeId(eq[0]); EqualityNodeId b = getNodeId(eq[1]); @@ -432,8 +432,8 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { EqualityNodeId bClassId = getEqualityNode(b).getFind(); if (d_isConstant[aClassId] && d_isConstant[bClassId]) { return; - } - + } + // If we are adding a disequality, notify of the shared term representatives EqualityNodeId eqId = getNodeId(eq); TriggerTermSetRef aTriggerRef = d_nodeIndividualTrigger[aClassId]; @@ -443,16 +443,16 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { // The sets of trigger terms TriggerTermSet& aTriggerTerms = getTriggerTermSet(aTriggerRef); TriggerTermSet& bTriggerTerms = getTriggerTermSet(bTriggerRef); - // Go through and notify the shared dis-equalities - Theory::Set aTags = aTriggerTerms.tags; - Theory::Set bTags = bTriggerTerms.tags; + // Go through and notify the shared dis-equalities + Theory::Set aTags = aTriggerTerms.tags; + Theory::Set bTags = bTriggerTerms.tags; TheoryId aTag = Theory::setPop(aTags); TheoryId bTag = Theory::setPop(bTags); int a_i = 0, b_i = 0; while (aTag != THEORY_LAST && bTag != THEORY_LAST) { if (aTag < bTag) { aTag = Theory::setPop(aTags); - ++ a_i; + ++ a_i; } else if (aTag > bTag) { bTag = Theory::setPop(bTags); ++ b_i; @@ -499,7 +499,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl; Assert(triggersFired.empty()); - + ++ d_stats.mergesCount; EqualityNodeId class1Id = class1.getFind(); @@ -539,8 +539,8 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect TaggedEqualitiesSet class1disequalitiesToNotify; // Individual tags - Theory::Set class1OnlyTags = Theory::setDifference(class1Tags, class2Tags); - Theory::Set class2OnlyTags = Theory::setDifference(class2Tags, class1Tags); + Theory::Set class1OnlyTags = Theory::setDifference(class1Tags, class2Tags); + Theory::Set class2OnlyTags = Theory::setDifference(class2Tags, class1Tags); // Only get disequalities if they are not both constant if (!class1isConstant || !class2isConstant) { @@ -590,9 +590,9 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl; do { // Get the current node - EqualityNode& currentNode = getEqualityNode(currentId); + EqualityNode& currentNode = getEqualityNode(currentId); Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl; - + // Go through the uselist and check for congruences UseListNodeId currentUseId = currentNode.getUseList(); while (currentUseId != null_uselist_id) { @@ -604,7 +604,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized; // If it's interpreted and we can interpret if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) { - // Get the actual term id + // Get the actual term id TNode term = d_nodes[funId]; subtermEvaluates(getNodeId(term)); } @@ -622,16 +622,16 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // There is no representative, so we can add one, we remove this when backtracking storeApplicationLookup(funNormalized, funId); } - + // Go to the next one in the use list currentUseId = useNode.getNext(); } - + // Move to the next node currentId = currentNode.getNext(); } while (currentId != class2Id); } - + // Now merge the lists class1.merge<true>(class2); @@ -660,24 +660,24 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Get the triggers TriggerTermSet& class1triggers = getTriggerTermSet(class1triggerRef); TriggerTermSet& class2triggers = getTriggerTermSet(class2triggerRef); - + // Initialize the merged set d_newSetTags = Theory::setUnion(class1triggers.tags, class2triggers.tags); d_newSetTriggersSize = 0; - + int i1 = 0; int i2 = 0; Theory::Set tags1 = class1triggers.tags; Theory::Set tags2 = class2triggers.tags; TheoryId tag1 = Theory::setPop(tags1); TheoryId tag2 = Theory::setPop(tags2); - + // Comparing the THEORY_LAST is OK because all other theories are // smaller, and will therefore be preferred - while (tag1 != THEORY_LAST || tag2 != THEORY_LAST) + while (tag1 != THEORY_LAST || tag2 != THEORY_LAST) { if (tag1 < tag2) { - // copy tag1 + // copy tag1 d_newSetTriggers[d_newSetTriggersSize++] = class1triggers.triggers[i1++]; tag1 = Theory::setPop(tags1); } else if (tag1 > tag2) { @@ -685,7 +685,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect d_newSetTriggers[d_newSetTriggersSize++] = class2triggers.triggers[i2++]; tag2 = Theory::setPop(tags2); } else { - // copy tag1 + // copy tag1 EqualityNodeId tag1id = d_newSetTriggers[d_newSetTriggersSize++] = class1triggers.triggers[i1++]; // since they are both tagged notify of merge if (d_performNotify) { @@ -698,17 +698,17 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect tag1 = Theory::setPop(tags1); tag2 = Theory::setPop(tags2); } - } - + } + // Add the new trigger set, if different from previous one if (class1triggers.tags != class2triggers.tags) { // Add it to the list for backtracking d_triggerTermSetUpdates.push_back(TriggerSetUpdate(class1Id, class1triggerRef)); d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1; - // Mark the the new set as a trigger + // Mark the the new set as a trigger d_nodeIndividualTrigger[class1Id] = newTriggerTermSet(); - } - } + } + } } // Everything fine @@ -792,14 +792,14 @@ void EqualityEngine::backtrack() { } d_triggerTermSetUpdates.resize(d_triggerTermSetUpdatesSize); } - + if (d_equalityTriggers.size() > d_equalityTriggersCount) { // Unlink the triggers from the lists for (int i = d_equalityTriggers.size() - 1, i_end = d_equalityTriggersCount; i >= i_end; -- i) { const Trigger& trigger = d_equalityTriggers[i]; d_nodeTriggers[trigger.classId] = trigger.nextTrigger; } - // Get rid of the triggers + // Get rid of the triggers d_equalityTriggers.resize(d_equalityTriggersCount); d_equalityTriggersOriginal.resize(d_equalityTriggersCount); } @@ -859,7 +859,7 @@ void EqualityEngine::backtrack() { d_deducedDisequalityReasons.resize(d_deducedDisequalityReasonsSize); d_deducedDisequalities.resize(d_deducedDisequalitiesSize); } - + } void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) { @@ -892,7 +892,7 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const { return out.str(); } -void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities) const { +void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities, EqProof * eqp) const { Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << std::endl; // The terms must be there already @@ -904,7 +904,7 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec if (polarity) { // Get the explanation - getExplanation(t1Id, t2Id, equalities); + getExplanation(t1Id, t2Id, equalities, eqp); } else { // Get the reason for this disequality EqualityPair pair(t1Id, t2Id); @@ -912,20 +912,20 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second; for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) { EqualityPair toExplain = d_deducedDisequalityReasons[i]; - getExplanation(toExplain.first, toExplain.second, equalities); + getExplanation(toExplain.first, toExplain.second, equalities, eqp); } } } -void EqualityEngine::explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions) const { +void EqualityEngine::explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, EqProof * eqp) const { Debug("equality") << d_name << "::eq::explainPredicate(" << p << ")" << std::endl; // Must have the term Assert(hasTerm(p)); // Get the explanation - getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions); + getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions, eqp); } -void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const { +void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof * eqp) const { Debug("equality") << d_name << "::eq::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl; @@ -933,17 +933,23 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st #ifdef CVC4_ASSERTIONS bool canExplain = getEqualityNode(t1Id).getFind() == getEqualityNode(t2Id).getFind() || (d_done && isConstant(t1Id) && isConstant(t2Id)); - + if (!canExplain) { Warning() << "Can't explain equality:" << std::endl; Warning() << d_nodes[t1Id] << " with find " << d_nodes[getEqualityNode(t1Id).getFind()] << std::endl; - Warning() << d_nodes[t2Id] << " with find " << d_nodes[getEqualityNode(t2Id).getFind()] << std::endl; + Warning() << d_nodes[t2Id] << " with find " << d_nodes[getEqualityNode(t2Id).getFind()] << std::endl; } Assert(canExplain); #endif // If the nodes are the same, we're done - if (t1Id == t2Id) return; + if (t1Id == t2Id){ + if( eqp ) { + eqp->d_node = d_nodes[t1Id]; + } + return; + } + if (Debug.isOn("equality::internal")) { debugPrintGraph(); @@ -986,6 +992,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl; + std::vector< EqProof * > eqp_trans; + // Reconstruct the path do { // The current node @@ -995,6 +1003,12 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl; + EqProof * eqpc = NULL; + //make child proof if a proof is being constructed + if( eqp ){ + eqpc = new EqProof; + eqpc->d_id = reasonType; + } // Add the actual equality to the vector switch (reasonType) { case MERGED_THROUGH_CONGRUENCE: { @@ -1003,32 +1017,45 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st const FunctionApplication& f1 = d_applications[currentNode].original; const FunctionApplication& f2 = d_applications[edgeNode].original; Debug("equality") << push; - getExplanation(f1.a, f2.a, equalities); - getExplanation(f1.b, f2.b, equalities); + EqProof * eqpc1 = eqpc ? new EqProof : NULL; + getExplanation(f1.a, f2.a, equalities, eqpc1); + EqProof * eqpc2 = eqpc ? new EqProof : NULL; + getExplanation(f1.b, f2.b, equalities, eqpc2); + if( eqpc ){ + eqpc->d_children.push_back( eqpc1 ); + eqpc->d_children.push_back( eqpc2 ); + } Debug("equality") << pop; break; - } + } case MERGED_THROUGH_EQUALITY: // Construct the equality Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl; + if( eqpc ){ + eqpc->d_node = d_equalityEdges[currentEdge].getReason(); + } equalities.push_back(d_equalityEdges[currentEdge].getReason()); break; case MERGED_THROUGH_REFLEXIVITY: { - // x1 == x1 + // x1 == x1 Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl; EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode; const FunctionApplication& eq = d_applications[eqId].original; Assert(eq.isEquality(), "Must be an equality"); - + // Explain why a = b constant Debug("equality") << push; - getExplanation(eq.a, eq.b, equalities); + EqProof * eqpc1 = eqpc ? new EqProof : NULL; + getExplanation(eq.a, eq.b, equalities, eqpc1); + if( eqpc ){ + eqpc->d_children.push_back( eqpc1 ); + } Debug("equality") << pop; - - break; + + break; } case MERGED_THROUGH_CONSTANTS: { - // f(c1, ..., cn) = c semantically, we can just ignore it + // f(c1, ..., cn) = c semantically, we can just ignore it Debug("equality") << d_name << "::eq::getExplanation(): due to constants, explain the constants" << std::endl; Debug("equality") << push; @@ -1042,7 +1069,11 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st for (unsigned i = 0; i < interpreted.getNumChildren(); ++ i) { EqualityNodeId childId = getNodeId(interpreted[i]); Assert(isConstant(childId)); - getExplanation(childId, getEqualityNode(childId).getFind(), equalities); + EqProof * eqpcc = eqpc ? new EqProof : NULL; + getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc); + if( eqpc ) { + eqpc->d_children.push_back( eqpcc ); + } } Debug("equality") << pop; @@ -1051,14 +1082,21 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st } default: Unreachable(); - } - + } + // Go to the previous currentEdge = bfsQueue[currentIndex].edgeId; currentIndex = bfsQueue[currentIndex].previousIndex; - + + eqp_trans.push_back( eqpc ); + } while (currentEdge != null_id); + if( eqp ){ + eqp->d_id = MERGED_THROUGH_TRANS; + eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() ); + } + // Done return; } @@ -1220,7 +1258,7 @@ void EqualityEngine::processEvaluationQueue() { // Get the node EqualityNodeId id = d_evaluationQueue.front(); d_evaluationQueue.pop(); - + // Replace the children with their representatives (must be constants) Node nodeEvaluated = evaluateTerm(d_nodes[id]); Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): " << d_nodes[id] << " evaluates to " << nodeEvaluated << std::endl; @@ -1240,11 +1278,11 @@ void EqualityEngine::propagate() { if (d_inPropagate) { // We're already in propagate, go back return; - } - + } + // Make sure we don't get in again ScopedBool inPropagate(d_inPropagate, true); - + Debug("equality") << d_name << "::eq::propagate()" << std::endl; while (!d_propagationQueue.empty() || !d_evaluationQueue.empty()) { @@ -1255,13 +1293,13 @@ void EqualityEngine::propagate() { while (!d_evaluationQueue.empty()) d_evaluationQueue.pop(); continue; } - + // Process any evaluation requests if (!d_evaluationQueue.empty()) { processEvaluationQueue(); continue; } - + // The current merge candidate const MergeCandidate current = d_propagationQueue.front(); d_propagationQueue.pop_front(); @@ -1288,7 +1326,7 @@ void EqualityEngine::propagate() { // Add the actual equality to the equality graph addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason); - // If constants are being merged we're done + // If constants are being merged we're done if (d_isConstant[t1classId] && d_isConstant[t2classId]) { // When merging constants we are inconsistent, hence done d_done = true; @@ -1462,7 +1500,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const return true; } } - + // Check the other equality itself if it exists eq = t2.eqNode(t1); if (hasTerm(eq)) { @@ -1474,7 +1512,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const return true; } } - + // Create the equality FunctionApplication eqNormalized(APP_EQUALITY, t1ClassId, t2ClassId); ApplicationIdsMap::const_iterator find = d_applicationLookup.find(eqNormalized); @@ -1492,7 +1530,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const return true; } } - + // Check the symmetric disequality std::swap(eqNormalized.a, eqNormalized.b); find = d_applicationLookup.find(eqNormalized); @@ -1510,7 +1548,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const return true; } } - + // Couldn't deduce dis-equalityReturn whether the terms are disequal return false; } @@ -1568,19 +1606,19 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // Initialize the new set for copy/insert d_newSetTags = Theory::setInsert(tag, triggerSet.tags); d_newSetTriggersSize = 0; - // Copy into to new one, and insert the new tag/id + // Copy into to new one, and insert the new tag/id unsigned i = 0; Theory::Set tags = d_newSetTags; - TheoryId current; + TheoryId current; while ((current = Theory::setPop(tags)) != THEORY_LAST) { // Remove from the tags tags = Theory::setRemove(current, tags); // Insert the id into the triggers - d_newSetTriggers[d_newSetTriggersSize++] = + d_newSetTriggers[d_newSetTriggersSize++] = current == tag ? eqNodeId : triggerSet.triggers[i++]; } } else { - // Setup a singleton + // Setup a singleton d_newSetTags = Theory::setInsert(tag); d_newSetTriggers[0] = eqNodeId; d_newSetTriggersSize = 1; @@ -1589,7 +1627,7 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // Add it to the list for backtracking d_triggerTermSetUpdates.push_back(TriggerSetUpdate(classId, triggerSetRef)); d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1; - // Mark the the new set as a trigger + // Mark the the new set as a trigger d_nodeIndividualTrigger[classId] = triggerSetRef = newTriggerTermSet(); // Propagate trigger term disequalities we remembered @@ -1843,7 +1881,7 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI } bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify) { - + // No tags, no food if (!tags) { return !d_done; @@ -1852,14 +1890,14 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger Assert(triggerSetRef != null_set_id); // This is the class trigger set - const TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef); + const TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef); // Go through the disequalities and notify TaggedEqualitiesSet::const_iterator it = disequalitiesToNotify.begin(); TaggedEqualitiesSet::const_iterator it_end = disequalitiesToNotify.end(); for (; !d_done && it != it_end; ++ it) { // The information about the equality that is asserted to false const TaggedEquality& disequalityInfo = *it; - const TriggerTermSet& disequalityTriggerSet = getTriggerTermSet(disequalityInfo.triggerSetRef); + const TriggerTermSet& disequalityTriggerSet = getTriggerTermSet(disequalityInfo.triggerSetRef); Theory::Set commonTags = Theory::setIntersection(disequalityTriggerSet.tags, tags); Assert(commonTags); // This is the actual function @@ -1897,7 +1935,7 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger } } } - + return !d_done; } @@ -2005,6 +2043,25 @@ bool EqClassIterator::isFinished() const { } +void EqProof::debug_print( const char * c, unsigned tb ){ + for( unsigned i=0; i<tb; i++ ) { Debug( c ) << " "; } + Debug( c ) << d_id << "("; + if( !d_children.empty() || !d_node.isNull() ){ + if( !d_node.isNull() ){ + Debug( c ) << std::endl; + for( unsigned i=0; i<tb+1; i++ ) { Debug( c ) << " "; } + Debug( c ) << d_node; + } + for( unsigned i=0; i<d_children.size(); i++ ){ + if( i>0 || !d_node.isNull() ) Debug( c ) << ","; + std::cout << std::endl; + d_children[i]->debug_print( c, tb+1 ); + } + } + Debug( c ) << ")"; +} + + } // Namespace uf } // Namespace theory } // Namespace CVC4 diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index ab106bc8d..f8e361081 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -39,6 +39,8 @@ namespace CVC4 { namespace theory { namespace eq { + +class EqProof; class EqClassesIterator; class EqClassIterator; @@ -421,35 +423,35 @@ private: /** * Map from ids of proper terms, to the number of non-constant direct subterms. If we update an interpreted * application to a constant, we can decrease this value. If we hit 0, we can evaluate the term. - * + * */ std::vector<unsigned> d_subtermsToEvaluate; - - /** + + /** * For nodes that we need to postpone evaluation. */ std::queue<EqualityNodeId> d_evaluationQueue; - + /** * Evaluate all terms in the evaluation queue. */ void processEvaluationQueue(); - + /** Vector of nodes that evaluate. */ std::vector<EqualityNodeId> d_subtermEvaluates; /** Size of the nodes that evaluate vector. */ context::CDO<unsigned> d_subtermEvaluatesSize; - + /** Set the node evaluate flag */ void subtermEvaluates(EqualityNodeId id); /** - * Returns the evaluation of the term when all (direct) children are replaced with + * Returns the evaluation of the term when all (direct) children are replaced with * the constant representatives. */ Node evaluateTerm(TNode node); - + /** * Returns true if it's a constant */ @@ -487,7 +489,7 @@ private: /** Enqueue to the propagation queue */ void enqueue(const MergeCandidate& candidate, bool back = true); - + /** Do the propagation */ void propagate(); @@ -499,7 +501,7 @@ private: * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere * else. */ - void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const; + void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof * eqp) const; /** * Print the equality graph. @@ -752,7 +754,7 @@ public: void assertPredicate(TNode p, bool polarity, TNode reason); /** - * Adds predicate p and q and makes them equal. + * Adds predicate p and q and makes them equal. */ void mergePredicates(TNode p, TNode q, TNode reason); @@ -782,14 +784,14 @@ public: * Returns the reasons (added when asserting) that imply it * in the assertions vector. */ - void explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& assertions) const; + void explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& assertions, EqProof * eqp = NULL) const; /** * Get an explanation of the predicate being true or false. * Returns the reasons (added when asserting) that imply imply it * in the assertions vector. */ - void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions) const; + void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, EqProof * eqp = NULL) const; /** * Add term to the set of trigger terms with a corresponding tag. The notify class will get @@ -890,6 +892,16 @@ public: bool isFinished() const; };/* class EqClassIterator */ +class EqProof +{ +public: + EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){} + MergeReasonType d_id; + Node d_node; + std::vector< EqProof * > d_children; + void debug_print( const char * c, unsigned tb = 0 ); +}; + } // Namespace eq } // Namespace theory } // Namespace CVC4 diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index a36291974..435a1ece5 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -54,7 +54,7 @@ static const EqualityEdgeId null_edge = (EqualityEdgeId)(-1); /** * A reason for a merge. Either an equality x = y, a merge of two - * function applications f(x1, x2), f(y1, y2) due to congruence, + * function applications f(x1, x2), f(y1, y2) due to congruence, * or a merge of an equality to false due to both sides being * (different) constants. */ @@ -67,6 +67,9 @@ enum MergeReasonType { MERGED_THROUGH_REFLEXIVITY, /** Equality was merged to false, due to both sides of equality being a constant */ MERGED_THROUGH_CONSTANTS, + + /** (for proofs only) Equality was merged due to transitivity */ + MERGED_THROUGH_TRANS, }; inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { @@ -83,6 +86,10 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { case MERGED_THROUGH_CONSTANTS: out << "constants disequal"; break; + // (for proofs only) + case MERGED_THROUGH_TRANS: + out << "transitivity"; + break; default: Unreachable(); } @@ -98,7 +105,7 @@ struct MergeCandidate { MergeReasonType type; TNode reason; MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason) - : t1Id(x), t2Id(y), type(type), reason(reason) + : t1Id(x), t2Id(y), type(type), reason(reason) {} }; @@ -112,9 +119,9 @@ struct DisequalityReasonRef { : mergesStart(mergesStart), mergesEnd(mergesEnd) {} }; -/** +/** * We maintain uselist where a node appears in, and this is the node - * of such a list. + * of such a list. */ class UseListNode { @@ -150,12 +157,12 @@ public: }; /** - * Main class for representing nodes in the equivalence class. The + * Main class for representing nodes in the equivalence class. The * nodes are a circular list, with the representative carrying the * size. Each individual node carries with itself the uselist of - * function applications it appears in and the list of asserted + * function applications it appears in and the list of asserted * disequalities it belongs to. In order to get these lists one must - * traverse the entire class and pick up all the individual lists. + * traverse the entire class and pick up all the individual lists. */ class EqualityNode { @@ -180,7 +187,7 @@ public: */ EqualityNode(EqualityNodeId nodeId = null_id) : d_size(1) - , d_findId(nodeId) + , d_findId(nodeId) , d_nextId(nodeId) , d_useList(null_uselist_id) {} @@ -232,7 +239,7 @@ public: /** * Note that this node is used in a function application funId, or - * a negatively asserted equality (dis-equality) with funId. + * a negatively asserted equality (dis-equality) with funId. */ template<typename memory_class> void usedIn(EqualityNodeId funId, memory_class& memory) { @@ -275,8 +282,8 @@ enum FunctionApplicationType { /** * Represents the function APPLY a b. If isEquality is true then it - * represents the predicate (a = b). Note that since one can not - * construct the equality over function terms, the equality and hash + * represents the predicate (a = b). Note that since one can not + * construct the equality over function terms, the equality and hash * function below are still well defined. */ struct FunctionApplication { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 1045c5a24..fd46ed7f4 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -178,10 +178,16 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) { // Do the work bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; + eq::EqProof * eqp = d_proofEnabled ? new eq::EqProof : NULL; if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp); } else { - d_equalityEngine.explainPredicate(atom, polarity, assumptions); + d_equalityEngine.explainPredicate(atom, polarity, assumptions, eqp); + } + //for now, just print debug + //TODO : send the proof outwards : d_out->conflict( lem, eqp ); + if( eqp ){ + eqp->debug_print("uf-pf"); } } @@ -462,6 +468,7 @@ void TheoryUF::computeCareGraph() { }/* TheoryUF::computeCareGraph() */ void TheoryUF::conflict(TNode a, TNode b) { + //TODO: create EqProof at this level if d_proofEnabled = true if (a.getKind() == kind::CONST_BOOLEAN) { d_conflictNode = explain(a.iffNode(b)); } else { diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 409b41e3f..3b59c1c58 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -346,23 +346,21 @@ void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground d_set_values[ isReq ? 1 : 0 ][ ground ? 1 : 0 ][n] = v; if( optUsePartialDefaults() ){ if( !ground ){ - if (!options::fmfFullModelCheck()) { - int defSize = (int)d_defaults.size(); - for( int i=0; i<defSize; i++ ){ - //for soundness, to allow variable order-independent function interpretations, - // we must ensure that the intersection of all default terms - // is also defined. - //for example, if we have that f( e, a ) = ..., and f( b, e ) = ..., - // then we must define f( b, a ). - bool isGround; - Node ni = getIntersection( m, n, d_defaults[i], isGround ); - if( !ni.isNull() ){ - //if the intersection exists, and is not already defined - if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() && - d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){ - //use the current value - setValue( m, ni, v, isGround, false ); - } + int defSize = (int)d_defaults.size(); + for( int i=0; i<defSize; i++ ){ + //for soundness, to allow variable order-independent function interpretations, + // we must ensure that the intersection of all default terms + // is also defined. + //for example, if we have that f( e, a ) = ..., and f( b, e ) = ..., + // then we must define f( b, a ). + bool isGround; + Node ni = getIntersection( m, n, d_defaults[i], isGround ); + if( !ni.isNull() ){ + //if the intersection exists, and is not already defined + if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() && + d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){ + //use the current value + setValue( m, ni, v, isGround, false ); } } } diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 052b2f568..a4cefe269 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1338,6 +1338,21 @@ void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality, d_sym_break_terms[n.getType()][sort_id].push_back( n ); d_sym_break_index[n] = use_cardinality; Trace("uf-ss-totality") << "Allocate symmetry breaking term " << n << ", index = " << use_cardinality << std::endl; + if( d_sym_break_terms[n.getType()][sort_id].size()>1 ){ + //enforce canonicity + for( int i=2; i<use_cardinality; i++ ){ + //can only be assigned to domain constant d if someone has been assigned domain constant d-1 + Node eq = n.eqNode( getTotalityLemmaTerm( cardinality, i ) ); + std::vector< Node > eqs; + for( unsigned j=0; j<(d_sym_break_terms[n.getType()][sort_id].size()-1); j++ ){ + eqs.push_back( d_sym_break_terms[n.getType()][sort_id][j].eqNode( getTotalityLemmaTerm( cardinality, i-1 ) ) ); + } + Node ax = NodeManager::currentNM()->mkNode( OR, eqs ); + Node lem = NodeManager::currentNM()->mkNode( IMPLIES, eq, ax ); + Trace("uf-ss-lemma") << "*** Add (canonicity) totality axiom " << lem << std::endl; + d_thss->getOutputChannel().lemma( lem ); + } + } } } @@ -1499,6 +1514,7 @@ void StrongSolverTheoryUF::newEqClass( Node n ){ if( options::ufssSymBreak() ){ d_sym_break->newEqClass( n ); } + Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl; } } @@ -1508,6 +1524,7 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){ if( c ){ Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl; c->merge( a, b ); + Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl; }else{ if( options::ufssDiseqPropagation() ){ d_deq_prop->merge(a, b); @@ -1523,6 +1540,7 @@ void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){ //Assert( d_th->d_equalityEngine.getRepresentative( a )==a ); //Assert( d_th->d_equalityEngine.getRepresentative( b )==b ); c->assertDisequal( a, b, reason ); + Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Assert disequal." << std::endl; }else{ if( options::ufssDiseqPropagation() ){ d_deq_prop->assertDisequal(a, b, reason); |