; 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)))
(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)
(! 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)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(! 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
;; ....
;; (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
;;
;; 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:
;;
;;))))))) (\ C
;;
;; C should be the clause (~v1 V v2 V ~v3 )
+
+
--- /dev/null
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
+;\r
+; Theory of Arrays\r
+;\r
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
+; depdends on : th_base.plf\r
+\r
+; sorts\r
+\r
+(declare array (! s1 sort (! s2 sort sort))) ; s1 is index, s2 is element\r
+\r
+; functions\r
+(declare write (! s1 sort\r
+ (! s2 sort\r
+ (! t1 (term (array s1 s2))\r
+ (! t2 (term s1)\r
+ (! t3 (term s2)\r
+ (term (array s1 s2))))))))\r
+(declare read (! s1 sort\r
+ (! s2 sort\r
+ (! t1 (term (array s1 s2))\r
+ (! t2 (term s1)\r
+ (term s2))))))\r
+ \r
+; inference rules\r
+(declare row1 (! s1 sort\r
+ (! s2 sort\r
+ (! t1 (term (array s1 s2))\r
+ (! t2 (term s1)\r
+ (! t3 (term s2)\r
+ (th_holds (= _ (read (write t1 t2 t3) t2) t3))))))))\r
+ \r
+\r
+(declare row (! s1 sort\r
+ (! s2 sort\r
+ (! t1 (term (array s1 s2))\r
+ (! t2 (term s1)\r
+ (! t3 (term s1)\r
+ (! t4 (term s2)\r
+ (! u (th_holds (not (= _ t2 t3)))\r
+ (th_holds (= _ (read (write t1 t2 t4) t3) (read t1 t3))))))))))\r
+\r
+(declare ext (! s1 sort\r
+ (! s2 sort\r
+ (! f formula\r
+ (! t1 (term (array s1 s2))\r
+ (! t2 (term (array s1 s2))\r
+ (! u (th_holds (not (= _ t1 t2)))\r
+ (! u1 (! k (term s1)\r
+ (! u2 (th_holds (not (= _ (read t1 k) (read t2 k))))\r
+ (th_holds f)))\r
+ (th_holds f)))))))))\r
+
\ No newline at end of file
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; 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
(! 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.
+; ...
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 \
setTimeLimit(options::cumulativeMillisecondLimit(), true);
}
- PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); );
+ PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); );
}
void SmtEngine::finalOptionsAreSet() {
}
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 );
// 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
// 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) {
finalOptionsAreSet();
doPendingPops();
- PROOF( ProofManager::currentPM()->addAssertion(ex); );
+ PROOF( ProofManager::currentPM()->addAssertion(ex); );
Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
#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
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 ){
}
}
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 ){
}
}
-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 ){
-
-
FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :
-FirstOrderModel(c, name), d_qe(qe){
+FirstOrderModel(qe, c, name){
}
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) {
}
}
-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());
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 );
+}
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:
/** 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 */
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 */
{
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;
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);
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 );
}
+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 */
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" );
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 );
}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
}
}
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() ){
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];
}
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;
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);
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);
bool QModelBuilder::optUseModel() {
- return options::fmfModelBasedInst() || options::fmfBoundInt();
+ return options::mbqiMode()!=MBQI_NONE || options::fmfBoundInt();
}
void QModelBuilder::debugModel( FirstOrderModel* fm ){
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
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 );
//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();
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 ){
#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;
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 );
}
}
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++ ){
#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 {
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 */
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 */
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
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
\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;
}
}
+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 */
--- /dev/null
+/********************* */\r
+/*! \file qinterval_builder.cpp\r
+ ** \verbatim\r
+ ** Original author: Andrew Reynolds\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Implementation of qinterval builder\r
+ **/\r
+\r
+\r
+#include "theory/quantifiers/qinterval_builder.h"\r
+\r
+using namespace std;\r
+using namespace CVC4;\r
+using namespace CVC4::kind;\r
+using namespace CVC4::context;\r
+using namespace CVC4::theory;\r
+using namespace CVC4::theory::quantifiers;\r
+\r
+//lower bound is exclusive\r
+//upper bound is inclusive\r
+\r
+struct QIntSort\r
+{\r
+ FirstOrderModelQInt * m;\r
+ bool operator() (Node i, Node j) {\r
+ return m->isLessThan( i, j );\r
+ }\r
+};\r
+\r
+void QIntDef::init_vec( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u ) {\r
+ for( unsigned i=0; i<m->getOrderedNumVars( q ); i++ ){\r
+ l.push_back( Node::null() );\r
+ u.push_back( m->getMaximum( m->getOrderedVarType( q, i ) ) );\r
+ }\r
+}\r
+\r
+void QIntDef::debugPrint( const char * c, FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u )\r
+{\r
+ Trace(c) << "( ";\r
+ for( unsigned i=0; i<l.size(); i++ ){\r
+ if( i>0 ) Trace(c) << ", ";\r
+ //Trace(c) << l[i] << "..." << u[i];\r
+ int lindex = l[i].isNull() ? 0 : m->getRepId( l[i] ) + 1;\r
+ int uindex = m->getRepId( u[i] );\r
+ Trace(c) << lindex << "..." << uindex;\r
+ }\r
+ Trace(c) << " )";\r
+}\r
+\r
+\r
+int QIntDef::getEvIndex( FirstOrderModelQInt * m, Node n, bool exc ) {\r
+ if( n.isNull() ){\r
+ Assert( exc );\r
+ return 0;\r
+ }else{\r
+ int min = 0;\r
+ int max = (int)(d_def_order.size()-1);\r
+ while( min!=max ){\r
+ int index = (min+max)/2;\r
+ Assert( index>=0 && index<(int)d_def_order.size() );\r
+ if( n==d_def_order[index] ){\r
+ max = index;\r
+ min = index;\r
+ }else if( m->isLessThan( n, d_def_order[index] ) ){\r
+ max = index;\r
+ }else{\r
+ min = index+1;\r
+ }\r
+ }\r
+ if( n==d_def_order[min] && exc ){\r
+ min++;\r
+ }\r
+ Assert( min>=0 && min<(int)d_def_order.size() );\r
+ if( ( min!=0 && !m->isLessThan( d_def_order[min-1], n ) && ( !exc || d_def_order[min-1]!=n ) ) ||\r
+ ( ( exc || d_def_order[min]!=n ) && !m->isLessThan( n, d_def_order[min] ) ) ){\r
+ Debug("qint-error") << "ERR size : " << d_def_order.size() << ", exc : " << exc << std::endl;\r
+ for( unsigned i=0; i<d_def_order.size(); i++ ){\r
+ Debug("qint-error") << "ERR ch #" << i << " : " << d_def_order[i];\r
+ Debug("qint-error") << " " << m->getRepId( d_def_order[i] ) << std::endl;\r
+ }\r
+ Debug("qint-error") << " : " << n << " " << min << " " << m->getRepId( n ) << std::endl;\r
+ }\r
+\r
+ Assert( min==0 || m->isLessThan( d_def_order[min-1], n ) || ( exc && d_def_order[min-1]==n ) );\r
+ Assert( ( !exc && n==d_def_order[min] ) || m->isLessThan( n, d_def_order[min] ) );\r
+ return min;\r
+ }\r
+}\r
+\r
+void QIntDef::addEntry( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,\r
+ Node v, unsigned depth ) {\r
+ if( depth==0 ){\r
+ Trace("qint-compose-debug") << "Add entry ";\r
+ debugPrint( "qint-compose-debug", m, q, l, u );\r
+ Trace("qint-compose-debug") << " -> " << v << "..." << std::endl;\r
+ }\r
+ //Assert( false );\r
+ if( depth==u.size() ){\r
+ Assert( d_def_order.empty() );\r
+ Assert( v.isNull() || v.isConst() || ( v.getType().isSort() && m->getRepId( v )!=-1 ) );\r
+ d_def_order.push_back( v );\r
+ }else{\r
+ /*\r
+ if( !d_def_order.empty() &&\r
+ ( l[depth].isNull() || m->isLessThan( l[depth], d_def_order[d_def_order.size()-1] ) ) ){\r
+ int startEvIndex = getEvIndex( m, l[depth], true );\r
+ int endEvIndex;\r
+ if( m->isLessThan( u[depth], d_def_order[d_def_order.size()-1] ) ){\r
+ endEvIndex = getEvIndex( m, u[depth] );\r
+ }else{\r
+ endEvIndex = d_def_order.size()-1;\r
+ }\r
+ Trace("qint-compose-debug2") << this << " adding for bounds " << l[depth] << "..." << u[depth] << std::endl;\r
+ for( int i=startEvIndex; i<=endEvIndex; i++ ){\r
+ Trace("qint-compose-debug2") << this << " add entry " << d_def_order[i] << std::endl;\r
+ d_def[d_def_order[i]].addEntry( m, q, l, u, v, depth+1 );\r
+ }\r
+ }\r
+ if( !d_def_order.empty() &&\r
+ d_def.find(u[depth])==d_def.end() &&\r
+ !m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){\r
+ Trace("qint-compose-debug2") << "Bad : depth : " << depth << std::endl;\r
+ }\r
+ Assert( d_def_order.empty() ||\r
+ d_def.find(u[depth])!=d_def.end() ||\r
+ m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) );\r
+\r
+ if( d_def_order.empty() || m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){\r
+ Trace("qint-compose-debug2") << this << " add entry new : " << u[depth] << std::endl;\r
+ d_def_order.push_back( u[depth] );\r
+ d_def[u[depth]].addEntry( m, q, l, u, v, depth+1 );\r
+ }\r
+ */\r
+ //%%%%%%\r
+ bool success = true;\r
+ int nnum = m->getVarOrder( q )->getNextNum( depth );\r
+ Node pl;\r
+ Node pu;\r
+ if( nnum!=-1 ){\r
+ Trace("qint-compose-debug2") << "...adding entry #" << depth << " is #" << nnum << std::endl;\r
+ //Assert( l[nnum].isNull() || l[nnum]==l[depth] || m->isLessThan( l[nnum], l[depth] ) );\r
+ //Assert( u[nnum]==u[depth] || m->isLessThan( u[depth], u[nnum] ) );\r
+ pl = l[nnum];\r
+ pu = u[nnum];\r
+ if( !m->doMeet( l[nnum], u[nnum], l[depth], u[depth], l[nnum], u[nnum] ) ){\r
+ success = false;\r
+ }\r
+ }\r
+ //%%%%%%\r
+ if( success ){\r
+ Node r = u[depth];\r
+ if( d_def.find( r )!=d_def.end() ){\r
+ d_def[r].addEntry( m, q, l, u, v, depth+1 );\r
+ }else{\r
+ if( !d_def_order.empty() &&\r
+ !m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){\r
+ Trace("qint-compose-debug2") << "Bad : depth : " << depth << " ";\r
+ Trace("qint-compose-debug2") << d_def_order[d_def_order.size()-1] << " " << u[depth] << std::endl;\r
+ }\r
+ Assert( d_def_order.empty() || m->isLessThan( d_def_order[d_def_order.size()-1], r ) );\r
+ d_def_order.push_back( r );\r
+ d_def[r].addEntry( m, q, l, u, v, depth+1 );\r
+ }\r
+ }\r
+ if( nnum!=-1 ){\r
+ l[nnum] = pl;\r
+ u[nnum] = pu;\r
+ }\r
+ }\r
+}\r
+\r
+Node QIntDef::simplify_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,\r
+ unsigned depth ) {\r
+ if( d_def.empty() ){\r
+ if( d_def_order.size()!=0 ){\r
+ Debug("qint-error") << "Simplify, size = " << d_def_order.size() << std::endl;\r
+ }\r
+ Assert( d_def_order.size()==1 );\r
+ return d_def_order[0];\r
+ }else{\r
+ Assert( !d_def_order.empty() );\r
+ std::vector< Node > newDefs;\r
+ Node curr;\r
+ for( unsigned i=0; i<d_def_order.size(); i++ ){\r
+ Node n = d_def[d_def_order[i]].simplify_r( m, q, il, iu, depth+1 );\r
+ if( i>0 ){\r
+ if( n==curr && !n.isNull() ){\r
+ d_def.erase( d_def_order[i-1] );\r
+ }else{\r
+ newDefs.push_back( d_def_order[i-1] );\r
+ }\r
+ }\r
+ curr = n;\r
+ }\r
+ newDefs.push_back( d_def_order[d_def_order.size()-1] );\r
+ d_def_order.clear();\r
+ d_def_order.insert( d_def_order.end(), newDefs.begin(), newDefs.end() );\r
+ return d_def_order.size()==1 ? curr : Node::null();\r
+ }\r
+}\r
+\r
+Node QIntDef::simplify( FirstOrderModelQInt * m, Node q ) {\r
+ std::vector< Node > l;\r
+ std::vector< Node > u;\r
+ if( !q.isNull() ){\r
+ //init_vec( m, q, l, u );\r
+ }\r
+ return simplify_r( m, q, l, u, 0 );\r
+}\r
+\r
+bool QIntDef::isTotal_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,\r
+ unsigned depth ) {\r
+ if( d_def_order.empty() ){\r
+ return false;\r
+ }else if( d_def.empty() ){\r
+ return true;\r
+ }else{\r
+ //get the current maximum\r
+ Node mx;\r
+ if( !q.isNull() ){\r
+ int pnum = m->getVarOrder( q )->getPrevNum( depth );\r
+ if( pnum!=-1 ){\r
+ mx = u[pnum];\r
+ }\r
+ }\r
+ if( mx.isNull() ){\r
+ mx = m->getMaximum( d_def_order[d_def_order.size()-1].getType() );\r
+ }\r
+ //if not current maximum\r
+ if( d_def_order[d_def_order.size()-1]!=mx ){\r
+ return false;\r
+ }else{\r
+ Node pu = u[depth];\r
+ for( unsigned i=0; i<d_def_order.size(); i++ ){\r
+ u[depth] = d_def_order[i];\r
+ if( !d_def[d_def_order[i]].isTotal_r( m, q, l, u, depth+1 ) ){\r
+ return false;\r
+ }\r
+ }\r
+ u[depth] = pu;\r
+ return true;\r
+ }\r
+ }\r
+}\r
+\r
+bool QIntDef::isTotal( FirstOrderModelQInt * m, Node q ) {\r
+ std::vector< Node > l;\r
+ std::vector< Node > u;\r
+ if( !q.isNull() ){\r
+ init_vec( m, q, l, u );\r
+ }\r
+ return isTotal_r( m, q, l, u, 0 );\r
+}\r
+\r
+void QIntDef::construct_compose_r( FirstOrderModelQInt * m, Node q,\r
+ std::vector< Node >& l, std::vector< Node >& u,\r
+ Node n, QIntDef * f,\r
+ std::vector< Node >& args,\r
+ std::map< unsigned, QIntDef >& children,\r
+ std::map< unsigned, Node >& bchildren,\r
+ QIntVarNumIndex& vindex, unsigned depth ) {\r
+ //check for short circuit\r
+ if( !f ){\r
+ if( !args.empty() ){\r
+ if( ( n.getKind()==OR && args[args.size()-1]==m->d_true ) ||\r
+ ( n.getKind()==AND && args[args.size()-1]==m->d_false ) ){\r
+ addEntry( m, q, l, u, args[args.size()-1] );\r
+ return;\r
+ }\r
+ }\r
+ }\r
+\r
+ for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << " "; }\r
+ Trace("qint-compose") << (f ? "U" : "I" ) << "C( ";\r
+ for( unsigned i=0; i<l.size(); i++ ){\r
+ if( i>0 ) Trace("qint-compose") << ", ";\r
+ //Trace("qint-compose") << l[i] << "..." << u[i];\r
+ int lindex = l[i].isNull() ? 0 : m->getRepId( l[i] ) + 1;\r
+ int uindex = m->getRepId( u[i] );\r
+ Trace( "qint-compose" ) << lindex << "..." << uindex;\r
+ }\r
+ Trace("qint-compose") << " )...";\r
+\r
+ //finished?\r
+ if( ( f && f->d_def.empty() ) || args.size()==n.getNumChildren() ){\r
+ if( f ){\r
+ Assert( f->d_def_order.size()==1 );\r
+ Trace("qint-compose") << "UVALUE(" << f->d_def_order[0] << ")" << std::endl;\r
+ addEntry( m, q, l, u, f->d_def_order[0] );\r
+ }else{\r
+ Node nn;\r
+ bool nnSet = false;\r
+ for( unsigned i=0; i<args.size(); i++ ){\r
+ if( args[i].isNull() ){\r
+ nnSet = true;\r
+ break;\r
+ }\r
+ }\r
+ if( !nnSet ){\r
+ if( n.getKind()==EQUAL ){\r
+ nn = NodeManager::currentNM()->mkConst( args[0]==args[1] );\r
+ }else{\r
+ //apply the operator to args\r
+ nn = NodeManager::currentNM()->mkNode( n.getKind(), args );\r
+ nn = Rewriter::rewrite( nn );\r
+ }\r
+ }\r
+ Trace("qint-compose") << "IVALUE(" << nn << ")" << std::endl;\r
+ addEntry( m, q, l, u, nn );\r
+ Trace("qint-compose-debug2") << "...added entry." << std::endl;\r
+ }\r
+ }else{\r
+ //if a non-simple child\r
+ if( children.find( depth )!=children.end() ){\r
+ //***************************\r
+ Trace("qint-compose") << "compound child, recurse" << std::endl;\r
+ std::vector< int > currIndex;\r
+ std::vector< int > endIndex;\r
+ std::vector< Node > prevL;\r
+ std::vector< Node > prevU;\r
+ std::vector< QIntDef * > visited;\r
+ do{\r
+ Assert( currIndex.size()==visited.size() );\r
+\r
+ //populate the vectors\r
+ while( visited.size()<m->getOrderedNumVars( q ) ){\r
+ unsigned i = visited.size();\r
+ QIntDef * qq = visited.empty() ? &children[depth] : visited[i-1]->getChild( currIndex[i-1] );\r
+ visited.push_back( qq );\r
+ Node qq_mx = qq->getMaximum();\r
+ Trace("qint-compose-debug2") << "...Get ev indices " << i << " " << l[i] << " " << u[i] << std::endl;\r
+ currIndex.push_back( qq->getEvIndex( m, l[i], true ) );\r
+ Trace("qint-compose-debug2") << "...Done get curr index " << currIndex[currIndex.size()-1] << std::endl;\r
+ if( m->isLessThan( qq_mx, u[i] ) ){\r
+ endIndex.push_back( qq->getNumChildren()-1 );\r
+ }else{\r
+ endIndex.push_back( qq->getEvIndex( m, u[i] ) );\r
+ }\r
+ Trace("qint-compose-debug2") << "...Done get end index " << endIndex[endIndex.size()-1] << std::endl;\r
+ prevL.push_back( l[i] );\r
+ prevU.push_back( u[i] );\r
+ if( !m->doMeet( prevL[i], prevU[i],\r
+ qq->getLower( currIndex[i] ), qq->getUpper( currIndex[i] ), l[i], u[i] ) ){\r
+ Assert( false );\r
+ }\r
+ }\r
+ for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << " "; }\r
+ for( unsigned i=0; i<currIndex.size(); i++ ){\r
+ Trace("qint-compose") << "[" << currIndex[i] << "/" << endIndex[i] << "]";\r
+ }\r
+ Trace("qint-compose") << std::endl;\r
+ //consider the current\r
+ int activeIndex = visited.size()-1;\r
+ QIntDef * qa = visited.empty() ? &children[depth] : visited[activeIndex]->getChild( currIndex[activeIndex] );\r
+ if( f ){\r
+ int fIndex = f->getEvIndex( m, qa->getValue() );\r
+ construct_compose_r( m, q, l, u, n, f->getChild( fIndex ), args, children, bchildren, vindex, depth+1 );\r
+ }else{\r
+ args.push_back( qa->getValue() );\r
+ construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, depth+1 );\r
+ args.pop_back();\r
+ }\r
+\r
+ //increment the index (if possible)\r
+ while( activeIndex>=0 && currIndex[activeIndex]==endIndex[activeIndex] ){\r
+ currIndex.pop_back();\r
+ endIndex.pop_back();\r
+ l[activeIndex] = prevL[activeIndex];\r
+ u[activeIndex] = prevU[activeIndex];\r
+ prevL.pop_back();\r
+ prevU.pop_back();\r
+ visited.pop_back();\r
+ activeIndex--;\r
+ }\r
+ if( activeIndex>=0 ){\r
+ for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << " "; }\r
+ Trace("qint-compose-debug") << "Increment at " << activeIndex << std::endl;\r
+ currIndex[activeIndex]++;\r
+ if( !m->doMeet( prevL[activeIndex], prevU[activeIndex],\r
+ visited[activeIndex]->getLower( currIndex[activeIndex] ),\r
+ visited[activeIndex]->getUpper( currIndex[activeIndex] ),\r
+ l[activeIndex], u[activeIndex] ) ){\r
+ Assert( false );\r
+ }\r
+ }\r
+ }while( !visited.empty() );\r
+ //***************************\r
+ }else{\r
+ Assert( bchildren.find( depth )!=bchildren.end() );\r
+ Node v = bchildren[depth];\r
+ if( f ){\r
+ if( v.getKind()==BOUND_VARIABLE ){\r
+ int vn = vindex.d_var_num[depth];\r
+ Trace("qint-compose") << "variable #" << vn << ", recurse" << std::endl;\r
+ //int vn = m->getOrderedVarOccurId( q, n, depth );\r
+ Trace("qint-compose-debug") << "-process " << v << ", which is var #" << vn << std::endl;\r
+ Node lprev = l[vn];\r
+ Node uprev = u[vn];\r
+ //restrict to last variable in order\r
+ int pnum = m->getVarOrder( q )->getPrevNum( vn );\r
+ if( pnum!=-1 ){\r
+ Trace("qint-compose-debug") << "-restrict to var #" << pnum << " " << l[pnum] << " " << u[pnum] << std::endl;\r
+ l[vn] = l[pnum];\r
+ u[vn] = u[pnum];\r
+ }\r
+ int startIndex = f->getEvIndex( m, l[vn], true );\r
+ int endIndex = f->getEvIndex( m, u[vn] );\r
+ Trace("qint-compose-debug") << "--will process " << startIndex << " " << endIndex << std::endl;\r
+ for( int i=startIndex; i<=endIndex; i++ ){\r
+ if( m->doMeet( lprev, uprev, f->getLower( i ), f->getUpper( i ), l[vn], u[vn] ) ){\r
+ construct_compose_r( m, q, l, u, n, f->getChild( i ), args, children, bchildren, vindex, depth+1 );\r
+ }else{\r
+ Assert( false );\r
+ }\r
+ }\r
+ l[vn] = lprev;\r
+ u[vn] = uprev;\r
+ }else{\r
+ Trace("qint-compose") << "value, recurse" << std::endl;\r
+ //simple\r
+ int ei = f->getEvIndex( m, v );\r
+ construct_compose_r( m, q, l, u, n, f->getChild( ei ), args, children, bchildren, vindex, depth+1 );\r
+ }\r
+ }else{\r
+ Trace("qint-compose") << "value, recurse" << std::endl;\r
+ args.push_back( v );\r
+ construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, depth+1 );\r
+ args.pop_back();\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+\r
+void QIntDef::construct_enum_r( FirstOrderModelQInt * m, Node q, unsigned vn, unsigned depth, Node v ) {\r
+ if( depth==m->getOrderedNumVars( q ) ){\r
+ Assert( !v.isNull() );\r
+ d_def_order.push_back( v );\r
+ }else{\r
+ TypeNode tn = m->getOrderedVarType( q, depth );\r
+ //int vnum = m->getVarOrder( q )->getVar( depth )==\r
+ if( depth==vn ){\r
+ for( unsigned i=0; i<m->d_rep_set.d_type_reps[tn].size(); i++ ){\r
+ Node vv = m->d_rep_set.d_type_reps[tn][i];\r
+ d_def_order.push_back( vv );\r
+ d_def[vv].construct_enum_r( m, q, vn, depth+1, vv );\r
+ }\r
+ }else if( m->getVarOrder( q )->getVar( depth )==m->getVarOrder( q )->getVar( vn ) && depth>vn ){\r
+ d_def_order.push_back( v );\r
+ d_def[v].construct_enum_r( m, q, vn, depth+1, v );\r
+ }else{\r
+ Node mx = m->getMaximum( tn );\r
+ d_def_order.push_back( mx );\r
+ d_def[mx].construct_enum_r( m, q, vn, depth+1, v );\r
+ }\r
+ }\r
+}\r
+\r
+bool QIntDef::construct_enum( FirstOrderModelQInt * m, Node q, unsigned vn ) {\r
+ TypeNode tn = m->getOrderedVarType( q, vn );\r
+ if( tn.isSort() ){\r
+ construct_enum_r( m, q, vn, 0, Node::null() );\r
+ return true;\r
+ }else{\r
+ return false;\r
+ }\r
+}\r
+\r
+bool QIntDef::construct_compose( FirstOrderModelQInt * m, Node q, Node n, QIntDef * f,\r
+ std::map< unsigned, QIntDef >& children,\r
+ std::map< unsigned, Node >& bchildren, int varChCount,\r
+ QIntVarNumIndex& vindex ) {\r
+ Trace("qint-compose") << "Do " << (f ? "uninterpreted" : "interpreted");\r
+ Trace("qint-compose") << " compose, var count = " << varChCount << "..." << std::endl;\r
+ std::vector< Node > l;\r
+ std::vector< Node > u;\r
+ init_vec( m, q, l, u );\r
+ if( varChCount==0 || f ){\r
+ //standard (no variable child) interpreted compose, or uninterpreted compose\r
+ std::vector< Node > args;\r
+ construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, 0 );\r
+ }else{\r
+ //special cases\r
+ bool success = false;\r
+ int varIndex = ( bchildren.find( 0 )!=bchildren.end() && bchildren[0].getKind()==BOUND_VARIABLE ) ? 0 : 1;\r
+ if( varChCount>1 ){\r
+ if( n.getKind()==EQUAL ){\r
+ //make it an enumeration\r
+ unsigned vn = vindex.d_var_num[0];\r
+ if( children[0].construct_enum( m, q, vn ) ){\r
+ bchildren.erase( 0 );\r
+ varIndex = 1;\r
+ success = true;\r
+ }\r
+ }\r
+ }else{\r
+ success = n.getKind()==EQUAL;\r
+ }\r
+ if( success ){\r
+ int oIndex = varIndex==0 ? 1 : 0;\r
+ Node v = bchildren[varIndex];\r
+ unsigned vn = vindex.d_var_num[varIndex];\r
+ if( children.find( oIndex )==children.end() ){\r
+ Assert( bchildren.find( oIndex )!=bchildren.end() );\r
+ Node at = bchildren[oIndex];\r
+ Trace("qint-icompose") << "Basic child, " << at << " with var " << v << std::endl;\r
+ Node prev = m->getPrev( bchildren[oIndex].getType(), bchildren[oIndex] );\r
+ Node above = u[vn];\r
+ if( !prev.isNull() ){\r
+ u[vn] = prev;\r
+ addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( false ) );\r
+ }\r
+ l[vn] = prev;\r
+ u[vn] = at;\r
+ addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( true ) );\r
+ if( at!=above ){\r
+ l[vn] = at;\r
+ u[vn] = above;\r
+ addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( false ) );\r
+ }\r
+ }else{\r
+ QIntDef * qid = &children[oIndex];\r
+ qid->debugPrint("qint-icompose", m, q );\r
+ Trace("qint-icompose") << " against variable..." << v << ", which is var #" << vn << std::endl;\r
+\r
+ TypeNode tn = v.getType();\r
+ QIntDefIter qdi( m, q, qid );\r
+ while( !qdi.isFinished() ){\r
+ std::vector< Node > us;\r
+ qdi.getUppers( us );\r
+ std::vector< Node > ls;\r
+ qdi.getLowers( ls );\r
+ qdi.debugPrint( "qint-icompose" );\r
+\r
+ Node n_below = ls[vn];\r
+ Node n_prev = m->getPrev( tn, qdi.getValue() );\r
+ Node n_at = qdi.getValue();\r
+ Node n_above = us[vn];\r
+ Trace("qint-icompose") << n_below << " < " << n_prev << " < " << n_at << " < " << n_above << std::endl;\r
+ if( n.getKind()==EQUAL ){\r
+ bool atLtAbove = m->isLessThan( n_at, n_above );\r
+ Node currL = n_below;\r
+ if( n_at==n_above || atLtAbove ){\r
+ //add for value (at-1)\r
+ if( !n_prev.isNull() && ( n_below.isNull() || m->isLessThan( n_below, n_prev ) ) ){\r
+ ls[vn] = currL;\r
+ us[vn] = n_prev;\r
+ currL = n_prev;\r
+ Trace("qint-icompose") << "-add entry(-) at " << ls[vn] << "..." << us[vn] << std::endl;\r
+ addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( false ) );\r
+ }\r
+ //add for value (at)\r
+ if( ( n_below.isNull() || m->isLessThan( n_below, n_at ) ) && atLtAbove ){\r
+ ls[vn] = currL;\r
+ us[vn] = n_at;\r
+ currL = n_at;\r
+ Trace("qint-icompose") << "-add entry(=) at " << ls[vn] << "..." << us[vn] << std::endl;\r
+ addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( true ) );\r
+ }\r
+ }\r
+ ls[vn] = currL;\r
+ us[vn] = n_above;\r
+ Trace("qint-icompose") << "-add entry(+) at " << ls[vn] << "..." << us[vn] << std::endl;\r
+ addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( n_at==n_above ) );\r
+ }else{\r
+ return false;\r
+ }\r
+ qdi.increment();\r
+\r
+ Trace("qint-icompose-debug") << "Now : " << std::endl;\r
+ debugPrint("qint-icompose-debug", m, q );\r
+ Trace("qint-icompose-debug") << std::endl;\r
+ }\r
+ }\r
+\r
+ Trace("qint-icompose") << "Result : " << std::endl;\r
+ debugPrint("qint-icompose", m, q );\r
+ Trace("qint-icompose") << std::endl;\r
+\r
+ }else{\r
+ return false;\r
+ }\r
+ }\r
+ Trace("qint-compose") << "Done i-compose" << std::endl;\r
+ return true;\r
+}\r
+\r
+\r
+void QIntDef::construct( FirstOrderModelQInt * m, std::vector< Node >& fapps, unsigned depth ) {\r
+ d_def.clear();\r
+ d_def_order.clear();\r
+ Assert( !fapps.empty() );\r
+ if( depth==fapps[0].getNumChildren() ){\r
+ //get representative in model for this term\r
+ Assert( fapps.size()>=1 );\r
+ Node r = m->getUsedRepresentative( fapps[0] );\r
+ d_def_order.push_back( r );\r
+ }else{\r
+ std::map< Node, std::vector< Node > > fapp_child;\r
+ //partition based on evaluations of fapps[1][depth]....fapps[n][depth]\r
+ for( unsigned i=0; i<fapps.size(); i++ ){\r
+ Node r = m->getUsedRepresentative( fapps[i][depth] );\r
+ fapp_child[r].push_back( fapps[i] );\r
+ }\r
+ //sort by QIntSort\r
+ for( std::map< Node, std::vector< Node > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){\r
+ d_def_order.push_back( it->first );\r
+ }\r
+ QIntSort qis;\r
+ qis.m = m;\r
+ std::sort( d_def_order.begin(), d_def_order.end(), qis );\r
+ //construct children\r
+ for( unsigned i=0; i<d_def_order.size(); i++ ){\r
+ Node n = d_def_order[i];\r
+ if( i==d_def_order.size()-1 ){\r
+ d_def_order[i] = m->getMaximum( d_def_order[i].getType() );\r
+ }\r
+ Debug("qint-model-debug2") << "Construct for " << n << ", terms = " << fapp_child[n].size() << std::endl;\r
+ d_def[d_def_order[i]].construct( m, fapp_child[n], depth+1 );\r
+ }\r
+ }\r
+}\r
+\r
+Node QIntDef::getFunctionValue( FirstOrderModelQInt * m, std::vector< Node >& vars, unsigned depth ) {\r
+ if( d_def.empty() ){\r
+ Assert( d_def_order.size()==1 );\r
+ //must convert to actual domain constant\r
+ if( d_def_order[0].getType().isSort() ){\r
+ return m->d_rep_set.d_type_reps[ d_def_order[0].getType() ][ m->getRepId( d_def_order[0] ) ];\r
+ }else{\r
+ return m->getUsedRepresentative( d_def_order[0] );\r
+ }\r
+ }else{\r
+ TypeNode tn = vars[depth].getType();\r
+ Node curr;\r
+ int rep_id = m->d_rep_set.getNumRepresentatives( tn );\r
+ for( int i=(int)(d_def_order.size()-1); i>=0; i-- ){\r
+ int curr_rep_id = i==0 ? 0 : m->getRepId( d_def_order[i-1] )+1;\r
+ Node ccurr = d_def[d_def_order[i]].getFunctionValue( m, vars, depth+1 );\r
+ if( curr.isNull() ){\r
+ curr = ccurr;\r
+ }else{\r
+ std::vector< Node > c;\r
+ Assert( curr_rep_id<rep_id );\r
+ for( int j=curr_rep_id; j<rep_id; j++ ){\r
+ c.push_back( vars[depth].eqNode( m->d_rep_set.d_type_reps[tn][j] ) );\r
+ }\r
+ Node cond = c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( OR, c );\r
+ curr = NodeManager::currentNM()->mkNode( ITE, cond, ccurr, curr );\r
+ }\r
+ rep_id = curr_rep_id;\r
+ }\r
+ return curr;\r
+ }\r
+}\r
+\r
+Node QIntDef::evaluate_r( FirstOrderModelQInt * m, std::vector< Node >& reps, unsigned depth ) {\r
+ if( depth==reps.size() ){\r
+ Assert( d_def_order.size()==1 );\r
+ return d_def_order[0];\r
+ }else{\r
+ if( d_def.find( reps[depth] )!=d_def.end() ){\r
+ return d_def[reps[depth]].evaluate_r( m, reps, depth+1 );\r
+ }else{\r
+ int ei = getEvIndex( m, reps[depth] );\r
+ return d_def[d_def_order[ei]].evaluate_r( m, reps, depth+1 );\r
+ }\r
+ }\r
+}\r
+Node QIntDef::evaluate_n_r( FirstOrderModelQInt * m, Node n, unsigned depth ) {\r
+ if( depth==n.getNumChildren() ){\r
+ Assert( d_def_order.size()==1 );\r
+ return d_def_order[0];\r
+ }else{\r
+ Node r = m->getUsedRepresentative( n[depth] );\r
+ if( d_def.find( r )!=d_def.end() ){\r
+ return d_def[r].evaluate_n_r( m, n, depth+1 );\r
+ }else{\r
+ int ei = getEvIndex( m, r );\r
+ return d_def[d_def_order[ei]].evaluate_n_r( m, n, depth+1 );\r
+ }\r
+ }\r
+}\r
+\r
+\r
+\r
+QIntDef * QIntDef::getChild( unsigned i ) {\r
+ Assert( i<d_def_order.size() );\r
+ Assert( d_def.find( d_def_order[i] )!=d_def.end() );\r
+ return &d_def[ d_def_order[i] ];\r
+}\r
+\r
+void QIntDef::debugPrint( const char * c, FirstOrderModelQInt * m, Node q, int t ) {\r
+ /*\r
+ for( unsigned i=0; i<d_def_order.size(); i++ ){\r
+ for( int j=0; j<t; j++ ) { Trace(c) << " "; }\r
+ //Trace(c) << this << " ";\r
+ Trace(c) << d_def_order[i] << " : " << std::endl;\r
+ if( d_def.find( d_def_order[i] )!=d_def.end() ){\r
+ d_def[d_def_order[i]].debugPrint( c, m, t+1 );\r
+ }\r
+ }\r
+ */\r
+ //if( t==0 ){\r
+ QIntDefIter qdi( m, q, this );\r
+ while( !qdi.isFinished() ){\r
+ qdi.debugPrint( c, t );\r
+ qdi.increment();\r
+ }\r
+ //}\r
+}\r
+\r
+\r
+QIntDefIter::QIntDefIter( FirstOrderModelQInt * m, Node q, QIntDef * qid ) : d_fm( m ), d_q( q ){\r
+ resetIndex( qid );\r
+}\r
+\r
+void QIntDefIter::debugPrint( const char * c, int t ) {\r
+ //Trace( c ) << getSize() << " " << d_index_visited.size() << " ";\r
+ for( int j=0; j<t; j++ ) { Trace(c) << " "; }\r
+ std::vector< Node > l;\r
+ std::vector< Node > u;\r
+ getLowers( l );\r
+ getUppers( u );\r
+ QIntDef::debugPrint( c, d_fm, d_q, l, u );\r
+ Trace( c ) << " -> " << getValue() << std::endl;\r
+}\r
+\r
+void QIntDefIter::resetIndex( QIntDef * qid ){\r
+ //std::cout << "check : " << qid << " " << qid->d_def_order.size() << " " << qid->d_def.size() << std::endl;\r
+ if( !qid->d_def.empty() ){\r
+ //std::cout << "add to visited " << qid << std::endl;\r
+ d_index.push_back( 0 );\r
+ d_index_visited.push_back( qid );\r
+ resetIndex( qid->getChild( 0 ) );\r
+ }\r
+}\r
+\r
+bool QIntDefIter::increment( int index ) {\r
+ if( !isFinished() ){\r
+ index = index==-1 ? (int)(d_index.size()-1) : index;\r
+ while( (int)(d_index.size()-1)>index ){\r
+ //std::cout << "remove from visit 1 " << std::endl;\r
+ d_index.pop_back();\r
+ d_index_visited.pop_back();\r
+ }\r
+ while( index>=0 && d_index[index]>=(int)(d_index_visited[index]->d_def_order.size()-1) ){\r
+ //std::cout << "remove from visit " << d_index_visited[ d_index_visited.size()-1 ] << std::endl;\r
+ d_index.pop_back();\r
+ d_index_visited.pop_back();\r
+ index--;\r
+ }\r
+ if( index>=0 ){\r
+ //std::cout << "increment at index = " << index << std::endl;\r
+ d_index[index]++;\r
+ resetIndex( d_index_visited[index]->getChild( d_index[index] ) );\r
+ return true;\r
+ }else{\r
+ d_index.clear();\r
+ return false;\r
+ }\r
+ }else{\r
+ return false;\r
+ }\r
+}\r
+\r
+Node QIntDefIter::getLower( int index ) {\r
+ if( d_index[index]==0 && !d_q.isNull() ){\r
+ int pnum = d_fm->getVarOrder( d_q )->getPrevNum( index );\r
+ if( pnum!=-1 ){\r
+ return getLower( pnum );\r
+ }\r
+ }\r
+ return d_index_visited[index]->getLower( d_index[index] );\r
+}\r
+\r
+Node QIntDefIter::getUpper( int index ) {\r
+ return d_index_visited[index]->getUpper( d_index[index] );\r
+}\r
+\r
+void QIntDefIter::getLowers( std::vector< Node >& reps ) {\r
+ for( unsigned i=0; i<getSize(); i++ ){\r
+ bool added = false;\r
+ if( d_index[i]==0 && !d_q.isNull() ){\r
+ int pnum = d_fm->getVarOrder( d_q )->getPrevNum( i );\r
+ if( pnum!=-1 ){\r
+ added = true;\r
+ reps.push_back( reps[pnum] );\r
+ }\r
+ }\r
+ if( !added ){\r
+ reps.push_back( getLower( i ) );\r
+ }\r
+ }\r
+}\r
+\r
+void QIntDefIter::getUppers( std::vector< Node >& reps ) {\r
+ for( unsigned i=0; i<getSize(); i++ ){\r
+ reps.push_back( getUpper( i ) );\r
+ }\r
+}\r
+\r
+Node QIntDefIter::getValue() {\r
+ return d_index_visited[ d_index_visited.size()-1 ]->getChild( d_index[d_index.size()-1] )->getValue();\r
+}\r
+\r
+\r
+//------------------------variable ordering----------------------------\r
+\r
+QuantVarOrder::QuantVarOrder( Node q ) : d_q( q ) {\r
+ d_var_count = 0;\r
+ initialize( q[1], 0, d_var_occur );\r
+}\r
+\r
+int QuantVarOrder::initialize( Node n, int minVarIndex, QIntVarNumIndex& vindex ) {\r
+ if( n.getKind()!=FORALL ){\r
+ //std::vector< Node > vars;\r
+ //std::vector< int > args;\r
+ int procVarOn = n.getKind()==APPLY_UF ? 0 : 1;\r
+ for( int r=0; r<=procVarOn; r++ ){\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ if( n[i].getKind()==BOUND_VARIABLE && r==procVarOn ){\r
+ int occ_index = -1;\r
+ for( unsigned j=0; j<d_var_to_num[n[i]].size(); j++ ){\r
+ if( d_var_to_num[n[i]][j]>=minVarIndex ){\r
+ occ_index = d_var_to_num[n[i]][j];\r
+ }\r
+ }\r
+ if( occ_index==-1 ){\r
+ //need to assign new\r
+ d_num_to_var[d_var_count] = n[i];\r
+ if( !d_var_to_num[n[i]].empty() ){\r
+ int v = d_var_to_num[n[i]][ d_var_to_num[n[i]].size()-1 ];\r
+ d_num_to_prev_num[ d_var_count ] = v;\r
+ d_num_to_next_num[ v ] = d_var_count;\r
+ }\r
+ d_var_num_index[ d_var_count ] = d_var_to_num[n[i]].size();\r
+ d_var_to_num[n[i]].push_back( d_var_count );\r
+ occ_index = d_var_count;\r
+ d_var_count++;\r
+ }\r
+ vindex.d_var_num[i] = occ_index;\r
+ minVarIndex = occ_index;\r
+ }else if( r==0 ){\r
+ minVarIndex = initialize( n[i], minVarIndex, vindex.d_var_index[i] );\r
+ }\r
+ }\r
+ }\r
+ }\r
+ return minVarIndex;\r
+}\r
+\r
+bool QuantVarOrder::getInstantiation( FirstOrderModelQInt * m, std::vector< Node >& l, std::vector< Node >& u,\r
+ std::vector< Node >& inst ) {\r
+ Debug("qint-var-order-debug2") << "Get for " << d_q << " " << l.size() << " " << u.size() << std::endl;\r
+ for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){\r
+ Debug("qint-var-order-debug2") << "Get for " << d_q[0][i] << " " << d_var_to_num[d_q[0][i]].size() << std::endl;\r
+ Node ll = Node::null();\r
+ Node uu = m->getMaximum( d_q[0][i].getType() );\r
+ for( unsigned j=0; j<d_var_to_num[d_q[0][i]].size(); j++ ){\r
+ Debug("qint-var-order-debug2") << "Go " << j << std::endl;\r
+ Node cl = ll;\r
+ Node cu = uu;\r
+ int index = d_var_to_num[d_q[0][i]][j];\r
+ Debug("qint-var-order-debug2") << "Do meet for " << index << "..." << std::endl;\r
+ Debug("qint-var-order-debug2") << l[index] << " " << u[index] << " " << cl << " " << cu << std::endl;\r
+ if( !m->doMeet( l[index], u[index], cl, cu, ll, uu ) ){\r
+ Debug("qint-var-order-debug2") << "FAILED" << std::endl;\r
+ return false;\r
+ }\r
+ Debug("qint-var-order-debug2") << "Result : " << ll << " " << uu << std::endl;\r
+ }\r
+ Debug("qint-var-order-debug2") << "Got " << uu << std::endl;\r
+ inst.push_back( uu );\r
+ }\r
+ return true;\r
+}\r
+\r
+void QuantVarOrder::debugPrint( const char * c ) {\r
+ Trace( c ) << "Variable order for " << d_q << " is : " << std::endl;\r
+ debugPrint( c, d_q[1], d_var_occur );\r
+ Trace( c ) << std::endl;\r
+ for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){\r
+ Trace( c ) << d_q[0][i] << " : ";\r
+ for( unsigned j=0; j<d_var_to_num[d_q[0][i]].size(); j++ ){\r
+ Trace( c ) << d_var_to_num[d_q[0][i]][j] << " ";\r
+ }\r
+ Trace( c ) << std::endl;\r
+ }\r
+}\r
+\r
+void QuantVarOrder::debugPrint( const char * c, Node n, QIntVarNumIndex& vindex ) {\r
+ if( n.getKind()==FORALL ){\r
+ Trace(c) << "NESTED_QUANT";\r
+ }else{\r
+ Trace(c) << n.getKind() << "(";\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ if( i>0 ) Trace( c ) << ",";\r
+ Trace( c ) << " ";\r
+ if( n[i].getKind()==BOUND_VARIABLE ){\r
+ Trace(c) << "VAR[" << vindex.d_var_num[i] << "]";\r
+ }else{\r
+ debugPrint( c, n[i], vindex.d_var_index[i] );\r
+ }\r
+ if( i==n.getNumChildren()-1 ) Trace( c ) << " ";\r
+ }\r
+ Trace(c) << ")";\r
+ }\r
+}\r
+\r
+QIntervalBuilder::QIntervalBuilder( context::Context* c, QuantifiersEngine* qe ) :\r
+QModelBuilder( c, qe ){\r
+ d_true = NodeManager::currentNM()->mkConst( true );\r
+}\r
+\r
+\r
+//------------------------model construction----------------------------\r
+\r
+void QIntervalBuilder::processBuildModel(TheoryModel* m, bool fullModel) {\r
+ Trace("fmf-qint-debug") << "process build model " << fullModel << std::endl;\r
+ FirstOrderModel* f = (FirstOrderModel*)m;\r
+ FirstOrderModelQInt* fm = f->asFirstOrderModelQInt();\r
+ if( fullModel ){\r
+ Trace("qint-model") << "Construct model representation..." << std::endl;\r
+ //make function values\r
+ for( std::map<Node, QIntDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {\r
+ if( it->first.getType().getNumChildren()>1 ){\r
+ Trace("qint-model") << "Construct for " << it->first << "..." << std::endl;\r
+ m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" );\r
+ }\r
+ }\r
+ TheoryEngineModelBuilder::processBuildModel( m, fullModel );\r
+ //mark that the model has been set\r
+ fm->markModelSet();\r
+ //debug the model\r
+ debugModel( fm );\r
+ }else{\r
+ fm->initialize( d_considerAxioms );\r
+ //process representatives\r
+ fm->d_rep_id.clear();\r
+ fm->d_max.clear();\r
+ fm->d_min.clear();\r
+ Trace("qint-model") << std::endl << "Making representatives..." << std::endl;\r
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();\r
+ it != fm->d_rep_set.d_type_reps.end(); ++it ){\r
+ if( it->first.isSort() ){\r
+ if( it->second.empty() ){\r
+ std::cout << "Empty rep for " << it->first << std::endl;\r
+ exit(0);\r
+ }\r
+ Trace("qint-model") << "Representatives for " << it->first << " : " << std::endl;\r
+ for( unsigned i=0; i<it->second.size(); i++ ){\r
+ Trace("qint-model") << i << " : " << it->second[i] << std::endl;\r
+ fm->d_rep_id[it->second[i]] = i;\r
+ }\r
+ fm->d_min[it->first] = it->second[0];\r
+ fm->d_max[it->first] = it->second[it->second.size()-1];\r
+ }else{\r
+ //TODO: enumerate?\r
+ }\r
+ }\r
+ Trace("qint-model") << std::endl << "Making function definitions..." << std::endl;\r
+ //construct the models for functions\r
+ for( std::map<Node, QIntDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {\r
+ Node f = it->first;\r
+ Trace("qint-model-debug") << "Building Model for " << f << std::endl;\r
+ //reset the model\r
+ //get all (non-redundant) f-applications\r
+ std::vector< Node > fapps;\r
+ Trace("qint-model-debug") << "Initial terms: " << std::endl;\r
+ for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){\r
+ Node n = fm->d_uf_terms[f][i];\r
+ if( !n.getAttribute(NoMatchAttribute()) ){\r
+ Trace("qint-model-debug") << " " << n << std::endl;\r
+ fapps.push_back( n );\r
+ }\r
+ }\r
+ if( fapps.empty() ){\r
+ //choose arbitrary value\r
+ Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);\r
+ Trace("qint-model-debug") << "Initial terms empty, add " << mbt << std::endl;\r
+ fapps.push_back( mbt );\r
+ }\r
+ //construct the interval model\r
+ it->second->construct( fm, fapps );\r
+ Trace("qint-model-debug") << "Definition for " << f << " : " << std::endl;\r
+ it->second->debugPrint("qint-model-debug", fm, Node::null() );\r
+\r
+ it->second->simplify( fm, Node::null() );\r
+ Trace("qint-model") << "(Simplified) definition for " << f << " : " << std::endl;\r
+ it->second->debugPrint("qint-model", fm, Node::null() );\r
+\r
+ if( Debug.isOn("qint-model-debug") ){\r
+ for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){\r
+ Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );\r
+ Debug("qint-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;\r
+ Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );\r
+ }\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+\r
+//--------------------model checking---------------------------------------\r
+\r
+//do exhaustive instantiation\r
+bool QIntervalBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {\r
+ Trace("qint-check") << "exhaustive instantiation " << q << " " << effort << std::endl;\r
+ if (effort==0) {\r
+\r
+ FirstOrderModelQInt * fmqint = fm->asFirstOrderModelQInt();\r
+ QIntDef qid;\r
+ doCheck( fmqint, q, qid, q[1], fmqint->d_var_order[q]->d_var_occur );\r
+ //now process entries\r
+ Trace("qint-inst") << "Interpretation for " << q << " is : " << std::endl;\r
+ qid.debugPrint( "qint-inst", fmqint, q );\r
+ Trace("qint-inst") << std::endl;\r
+ Debug("qint-check-debug2") << "Make iterator..." << std::endl;\r
+ QIntDefIter qdi( fmqint, q, &qid );\r
+ while( !qdi.isFinished() ){\r
+ if( qdi.getValue()!=d_true ){\r
+ Debug("qint-check-debug2") << "Set up vectors..." << std::endl;\r
+ std::vector< Node > l;\r
+ std::vector< Node > u;\r
+ std::vector< Node > inst;\r
+ qdi.getLowers( l );\r
+ qdi.getUppers( u );\r
+ Debug("qint-check-debug2") << "Get instantiation..." << std::endl;\r
+ if( fmqint->d_var_order[q]->getInstantiation( fmqint, l, u, inst ) ){\r
+ Trace("qint-inst") << "** Instantiate with ";\r
+ //just add the instance\r
+ InstMatch m;\r
+ for( unsigned j=0; j<inst.size(); j++) {\r
+ m.set( d_qe, q, j, inst[j] );\r
+ Trace("qint-inst") << inst[j] << " ";\r
+ }\r
+ Trace("qint-inst") << std::endl;\r
+ d_triedLemmas++;\r
+ if( d_qe->addInstantiation( q, m ) ){\r
+ Trace("qint-inst") << " ...added instantiation." << std::endl;\r
+ d_addedLemmas++;\r
+ }else{\r
+ Trace("qint-inst") << " ...duplicate instantiation" << std::endl;\r
+ //verify that instantiation is witness for current entry\r
+ if( Debug.isOn("qint-check-debug2") ){\r
+ Debug("qint-check-debug2") << "Check if : ";\r
+ std::vector< Node > exp_inst;\r
+ for( unsigned i=0; i<fmqint->getOrderedNumVars( q ); i++ ){\r
+ int index = fmqint->getOrderedVarNumToVarNum( q, i );\r
+ exp_inst.push_back( inst[ index ] );\r
+ Debug("qint-check-debug2") << inst[index] << " ";\r
+ }\r
+ Debug("qint-check-debug2") << " evaluates to " << qdi.getValue() << std::endl;\r
+ Assert( qid.evaluate( fmqint, exp_inst )==qdi.getValue() );\r
+ }\r
+ }\r
+ }else{\r
+ Trace("qint-inst") << "** Spurious instantiation." << std::endl;\r
+ }\r
+ }\r
+ qdi.increment();\r
+ }\r
+ }\r
+ return true;\r
+}\r
+\r
+bool QIntervalBuilder::doCheck( FirstOrderModelQInt * m, Node q, QIntDef & qid, Node n,\r
+ QIntVarNumIndex& vindex ) {\r
+ Assert( n.getKind()!=FORALL );\r
+ std::map< unsigned, QIntDef > children;\r
+ std::map< unsigned, Node > bchildren;\r
+ int varChCount = 0;\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ if( n[i].getKind()==FORALL ){\r
+ bchildren[i] = Node::null();\r
+ }else if( n[i].getKind() == BOUND_VARIABLE ){\r
+ varChCount++;\r
+ bchildren[i] = n[i];\r
+ }else if( m->hasTerm( n[i] ) ){\r
+ bchildren[i] = m->getUsedRepresentative( n[i] );\r
+ }else{\r
+ if( !doCheck( m, q, children[i], n[i], vindex.d_var_index[i] ) ){\r
+ bchildren[i] = Node::null();\r
+ }\r
+ }\r
+ }\r
+ Trace("qint-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl;\r
+ if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){\r
+ Node op = n.getKind() == APPLY_UF ? n.getOperator() : n;\r
+ //uninterpreted compose\r
+ qid.construct_compose( m, q, n, m->d_models[op], children, bchildren, varChCount, vindex );\r
+ }else if( !qid.construct_compose( m, q, n, NULL, children, bchildren, varChCount, vindex ) ){\r
+ Trace("qint-check-debug") << "** Cannot produce definition for " << n << std::endl;\r
+ return false;\r
+ }\r
+ Trace("qint-check-debug2") << "Definition for " << n << " is : " << std::endl;\r
+ qid.debugPrint("qint-check-debug2", m, q);\r
+ qid.simplify( m, q );\r
+ Trace("qint-check-debug") << "(Simplified) Definition for " << n << " is : " << std::endl;\r
+ qid.debugPrint("qint-check-debug", m, q);\r
+ Trace("qint-check-debug") << std::endl;\r
+ Assert( qid.isTotal( m, q ) );\r
+ return true;\r
+}\r
--- /dev/null
+/********************* */\r
+/*! \file qinterval_builder.h\r
+ ** \verbatim\r
+ ** Original author: Andrew Reynolds\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief qinterval model class\r
+ **/\r
+\r
+#include "cvc4_private.h"\r
+\r
+#ifndef QINTERVAL_BUILDER\r
+#define QINTERVAL_BUILDER\r
+\r
+#include "theory/quantifiers/model_builder.h"\r
+#include "theory/quantifiers/first_order_model.h"\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+namespace quantifiers {\r
+\r
+class FirstOrderModelQInt;\r
+\r
+class QIntVarNumIndex\r
+{\r
+public:\r
+ std::map< int, int > d_var_num;\r
+ std::map< int, QIntVarNumIndex > d_var_index;\r
+};\r
+\r
+class QIntDef\r
+{\r
+private:\r
+ Node evaluate_r( FirstOrderModelQInt * m, std::vector< Node >& reps, unsigned depth );\r
+ Node evaluate_n_r( FirstOrderModelQInt * m, Node n, unsigned depth );\r
+ void construct_compose_r( FirstOrderModelQInt * m, Node q,\r
+ std::vector< Node >& l, std::vector< Node >& u, Node n, QIntDef * f,\r
+ std::vector< Node >& args,\r
+ std::map< unsigned, QIntDef >& children,\r
+ std::map< unsigned, Node >& bchildren,\r
+ QIntVarNumIndex& vindex,\r
+ unsigned depth );\r
+\r
+ void construct_enum_r( FirstOrderModelQInt * m, Node q, unsigned vn, unsigned depth, Node v );\r
+ int getEvIndex( FirstOrderModelQInt * m, Node n, bool exc = false );\r
+ void addEntry( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,\r
+ Node v, unsigned depth = 0 );\r
+ Node simplify_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,\r
+ unsigned depth );\r
+ bool isTotal_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,\r
+ unsigned depth );\r
+public:\r
+ QIntDef(){}\r
+ std::map< Node, QIntDef > d_def;\r
+ std::vector< Node > d_def_order;\r
+\r
+ void construct( FirstOrderModelQInt * m, std::vector< Node >& fapps, unsigned depth = 0 );\r
+ bool construct_compose( FirstOrderModelQInt * m, Node q, Node n, QIntDef * f,\r
+ std::map< unsigned, QIntDef >& children,\r
+ std::map< unsigned, Node >& bchildren, int varChCount,\r
+ QIntVarNumIndex& vindex );\r
+ bool construct_enum( FirstOrderModelQInt * m, Node q, unsigned vn );\r
+\r
+ Node evaluate( FirstOrderModelQInt * m, std::vector< Node >& reps ) { return evaluate_r( m, reps, 0 ); }\r
+ Node evaluate_n( FirstOrderModelQInt * m, Node n ) { return evaluate_n_r( m, n, 0 ); }\r
+\r
+ void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, int t = 0 );\r
+ QIntDef * getChild( unsigned i );\r
+ Node getValue() { return d_def_order[0]; }\r
+ Node getLower( unsigned i ) { return i==0 ? Node::null() : d_def_order[i-1]; }\r
+ Node getUpper( unsigned i ) { return d_def_order[i]; }\r
+ Node getMaximum() { return d_def_order.empty() ? Node::null() : getUpper( d_def_order.size()-1 ); }\r
+ int getNumChildren() { return d_def_order.size(); }\r
+ bool isTotal( FirstOrderModelQInt * m, Node q );\r
+\r
+ Node simplify( FirstOrderModelQInt * m, Node q );\r
+ Node getFunctionValue( FirstOrderModelQInt * m, std::vector< Node >& vars, unsigned depth = 0 );\r
+\r
+ static void init_vec( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u );\r
+ static void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u );\r
+};\r
+\r
+class QIntDefIter {\r
+private:\r
+ FirstOrderModelQInt * d_fm;\r
+ Node d_q;\r
+ void resetIndex( QIntDef * qid );\r
+public:\r
+ QIntDefIter( FirstOrderModelQInt * m, Node q, QIntDef * qid );\r
+ void debugPrint( const char * c, int t = 0 );\r
+ std::vector< QIntDef * > d_index_visited;\r
+ std::vector< int > d_index;\r
+ bool isFinished() { return d_index.empty(); }\r
+ bool increment( int index = -1 );\r
+ unsigned getSize() { return d_index.size(); }\r
+ Node getLower( int index );\r
+ Node getUpper( int index );\r
+ void getLowers( std::vector< Node >& reps );\r
+ void getUppers( std::vector< Node >& reps );\r
+ Node getValue();\r
+};\r
+\r
+\r
+class QuantVarOrder\r
+{\r
+private:\r
+ int initialize( Node n, int minVarIndex, QIntVarNumIndex& vindex );\r
+ int d_var_count;\r
+ Node d_q;\r
+ void debugPrint( const char * c, Node n, QIntVarNumIndex& vindex );\r
+public:\r
+ QuantVarOrder( Node q );\r
+ std::map< int, Node > d_num_to_var;\r
+ std::map< int, int > d_num_to_prev_num;\r
+ std::map< int, int > d_num_to_next_num;\r
+ std::map< Node, std::vector< int > > d_var_to_num;\r
+ std::map< int, int > d_var_num_index;\r
+ //std::map< Node, std::map< int, int > > d_var_occur;\r
+ //int getVarNum( Node n, int arg ) { return d_var_occur[n][arg]; }\r
+ unsigned getNumVars() { return d_var_count; }\r
+ Node getVar( int i ) { return d_num_to_var[i]; }\r
+ 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; }\r
+ 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; }\r
+ int getVarNumIndex( int i ) { return d_var_num_index[i]; }\r
+ bool getInstantiation( FirstOrderModelQInt * m, std::vector< Node >& l, std::vector< Node >& u,\r
+ std::vector< Node >& inst );\r
+ void debugPrint( const char * c );\r
+ QIntVarNumIndex d_var_occur;\r
+};\r
+\r
+class QIntervalBuilder : public QModelBuilder\r
+{\r
+private:\r
+ Node d_true;\r
+ bool doCheck( FirstOrderModelQInt * m, Node q, QIntDef & qid, Node n,\r
+ QIntVarNumIndex& vindex );\r
+public:\r
+ QIntervalBuilder( context::Context* c, QuantifiersEngine* qe );\r
+ //process build model\r
+ void processBuildModel(TheoryModel* m, bool fullModel);\r
+ //do exhaustive instantiation\r
+ bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );\r
+};\r
+\r
+\r
+}\r
+}\r
+}\r
+\r
+#endif
\ No newline at end of file
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++;
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++;
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];
}
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
, d_sharedTerms(satContext)
, d_out(&out)
, d_valuation(valuation)
+ , d_proofEnabled(false)
{
StatisticsRegistry::registerStat(&d_computeCareGraphTime);
}
void printFacts(std::ostream& os) const;
void debugPrintFacts() const;
+ /**
+ * Whether proofs are enabled
+ *
+ */
+ bool d_proofEnabled;
+
public:
/**
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);
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]))) {
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();
}
propagate();
Assert(hasTerm(t));
-
+
Debug("equality") << d_name << "::eq::addTermInternal(" << t << ") => " << result << std::endl;
}
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]);
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];
// 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;
Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl;
Assert(triggersFired.empty());
-
+
++ d_stats.mergesCount;
EqualityNodeId class1Id = class1.getFind();
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) {
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) {
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));
}
// 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);
// 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) {
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) {
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
}
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);
}
d_deducedDisequalityReasons.resize(d_deducedDisequalityReasonsSize);
d_deducedDisequalities.resize(d_deducedDisequalitiesSize);
}
-
+
}
void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) {
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
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);
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;
#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();
Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl;
+ std::vector< EqProof * > eqp_trans;
+
// Reconstruct the path
do {
// The current node
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: {
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;
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;
}
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;
}
// 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;
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()) {
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();
// 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;
return true;
}
}
-
+
// Check the other equality itself if it exists
eq = t2.eqNode(t1);
if (hasTerm(eq)) {
return true;
}
}
-
+
// Create the equality
FunctionApplication eqNormalized(APP_EQUALITY, t1ClassId, t2ClassId);
ApplicationIdsMap::const_iterator find = d_applicationLookup.find(eqNormalized);
return true;
}
}
-
+
// Check the symmetric disequality
std::swap(eqNormalized.a, eqNormalized.b);
find = d_applicationLookup.find(eqNormalized);
return true;
}
}
-
+
// Couldn't deduce dis-equalityReturn whether the terms are disequal
return false;
}
// 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;
// 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
}
bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify) {
-
+
// No tags, no food
if (!tags) {
return !d_done;
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
}
}
}
-
+
return !d_done;
}
}
+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
namespace theory {
namespace eq {
+
+class EqProof;
class EqClassesIterator;
class EqClassIterator;
/**
* 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
*/
/** Enqueue to the propagation queue */
void enqueue(const MergeCandidate& candidate, bool back = true);
-
+
/** Do the propagation */
void propagate();
* 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.
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);
* 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
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
/**
* 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.
*/
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) {
case MERGED_THROUGH_CONSTANTS:
out << "constants disequal";
break;
+ // (for proofs only)
+ case MERGED_THROUGH_TRANS:
+ out << "transitivity";
+ break;
default:
Unreachable();
}
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)
{}
};
: 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 {
};
/**
- * 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 {
*/
EqualityNode(EqualityNodeId nodeId = null_id)
: d_size(1)
- , d_findId(nodeId)
+ , d_findId(nodeId)
, d_nextId(nodeId)
, d_useList(null_uselist_id)
{}
/**
* 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) {
/**
* 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 {
// 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");
}
}
}/* 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 {
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 );
}
}
}
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 );
+ }
+ }
}
}
if( options::ufssSymBreak() ){
d_sym_break->newEqClass( n );
}
+ Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl;
}
}
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);
//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);
projects / cvc5.git / commitdiff