diff options
Diffstat (limited to 'src/theory/quantifiers')
26 files changed, 1234 insertions, 1246 deletions
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index 2b16c9af3..3a19ff9c6 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -25,20 +25,18 @@ libquantifiers_la_SOURCES = \ inst_match.cpp \ model_engine.h \ model_engine.cpp \ - inst_when_mode.cpp \ - inst_when_mode.h \ - literal_match_mode.cpp \ - literal_match_mode.h \ + modes.cpp \ + modes.h \ relevant_domain.h \ relevant_domain.cpp \ - rep_set_iterator.h \ - rep_set_iterator.cpp \ term_database.h \ term_database.cpp \ first_order_model.h \ first_order_model.cpp \ model_builder.h \ - model_builder.cpp + model_builder.cpp \ + quantifiers_attributes.h \ + quantifiers_attributes.cpp EXTRA_DIST = \ kinds \ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index fd616948c..c3be1cdaf 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -15,9 +15,11 @@ **/ #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/rep_set_iterator.h" #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/quantifiers_attributes.h" + +#define USE_INDEX_ORDERING using namespace std; using namespace CVC4; @@ -26,39 +28,38 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -FirstOrderModel::FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ) : DefaultModel( c, name, true ), -d_term_db( qe->getTermDatabase() ), d_forall_asserts( c ){ +FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : DefaultModel( c, name, true ), +d_axiom_asserted( c, false ), d_forall_asserts( c ){ } +void FirstOrderModel::assertQuantifier( Node n ){ + d_forall_asserts.push_back( n ); + if( n.getAttribute(AxiomAttribute()) ){ + d_axiom_asserted = true; + } +} + void FirstOrderModel::reset(){ - //rebuild models - d_uf_model_tree.clear(); - d_uf_model_gen.clear(); - d_array_model.clear(); DefaultModel::reset(); } void FirstOrderModel::addTerm( Node n ){ - //std::vector< Node > added; - //d_term_db->addTerm( n, added, false ); DefaultModel::addTerm( n ); } -void FirstOrderModel::initialize(){ +void FirstOrderModel::initialize( bool considerAxioms ){ + //rebuild models + d_uf_model_tree.clear(); + d_uf_model_gen.clear(); + d_array_model.clear(); //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 ); - //initialize relevant models within bodies of all quantifiers - initializeModelForTerm( f[1] ); - } - //for debugging - if( Trace.isOn("model-engine") ){ - for( std::map< TypeNode, std::vector< Node > >::iterator it = d_rep_set.d_type_reps.begin(); it != d_rep_set.d_type_reps.end(); ++it ){ - if( it->first.isSort() ){ - Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; - } + if( considerAxioms || !f.hasAttribute(AxiomAttribute()) ){ + //initialize relevant models within bodies of all quantifiers + initializeModelForTerm( f[1] ); } } } @@ -92,33 +93,16 @@ void FirstOrderModel::initializeModelForTerm( Node n ){ } } -void FirstOrderModel::toStreamFunction( Node n, std::ostream& out ){ - /* - if( d_uf_model.find( n )!=d_uf_model.end() ){ - //d_uf_model[n].toStream( out ); - Node value = d_uf_model[n].getFunctionValue(); - out << "(" << n << " " << value << ")"; - }else if( d_array_model.find( n )!=d_array_model.end() ){ - Node value = d_array_model[n].getArrayValue(); - out << "(" << n << " " << value << ")" << std::endl; - } - */ - DefaultModel::toStreamFunction( n, out ); -} - -void FirstOrderModel::toStreamType( TypeNode tn, std::ostream& out ){ - DefaultModel::toStreamType( tn, out ); -} - Node FirstOrderModel::getInterpretedValue( TNode n ){ Debug("fo-model") << "get interpreted value " << n << std::endl; TypeNode type = n.getType(); if( type.isFunction() || type.isPredicate() ){ - if( d_uf_models.find( n )==d_uf_models.end() ){ - //use the model tree to generate the model - Node fn = d_uf_model_tree[n].getFunctionValue(); - d_uf_models[n] = fn; - return fn; + if( d_uf_model_tree.find( n )!=d_uf_model_tree.end() ){ + if( d_uf_models.find( n )==d_uf_models.end() ){ + //use the model tree to generate the model + d_uf_models[n] = d_uf_model_tree[n].getFunctionValue( "$x" ); + } + return d_uf_models[n]; } /* }else if( type.isArray() ){ @@ -141,44 +125,387 @@ Node FirstOrderModel::getInterpretedValue( TNode n ){ return DefaultModel::getInterpretedValue( n ); } -TermDb* FirstOrderModel::getTermDatabase(){ - return d_term_db; +void FirstOrderModel::toStream(std::ostream& out){ + } -void FirstOrderModel::toStream(std::ostream& out){ - DefaultModel::toStream( out ); +//for evaluation of quantifier bodies + +void FirstOrderModel::resetEvaluate(){ + d_eval_uf_use_default.clear(); + d_eval_uf_model.clear(); + d_eval_term_index_order.clear(); + d_eval_failed.clear(); + d_eval_failed_lits.clear(); + d_eval_formulas = 0; + d_eval_uf_terms = 0; + d_eval_lits = 0; + d_eval_lits_unknown = 0; +} + +//if evaluate( n ) = eVal, +// let n' = ri * n be the formula n instantiated with the current values in r_iter +// if eVal = 1, then n' is true, if eVal = -1, then n' is false, +// if eVal = 0, then n' cannot be proven to be equal to phaseReq +// if eVal is not 0, then +// each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model +int FirstOrderModel::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ + ++d_eval_formulas; + //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl; + //Notice() << "Eval " << n << std::endl; + if( n.getKind()==NOT ){ + int val = evaluate( n[0], depIndex, ri ); + return val==1 ? -1 : ( val==-1 ? 1 : 0 ); + }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){ + int baseVal = n.getKind()==AND ? 1 : -1; + int eVal = baseVal; + int posDepIndex = ri->getNumTerms(); + int negDepIndex = -1; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + //evaluate subterm + int childDepIndex; + Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i]; + int eValT = evaluate( nn, childDepIndex, ri ); + if( eValT==baseVal ){ + if( eVal==baseVal ){ + if( childDepIndex>negDepIndex ){ + negDepIndex = childDepIndex; + } + } + }else if( eValT==-baseVal ){ + eVal = -baseVal; + if( childDepIndex<posDepIndex ){ + posDepIndex = childDepIndex; + if( posDepIndex==-1 ){ + break; + } + } + }else if( eValT==0 ){ + if( eVal==baseVal ){ + eVal = 0; + } + } + } + if( eVal!=0 ){ + depIndex = eVal==-baseVal ? posDepIndex : negDepIndex; + return eVal; + }else{ + return 0; + } + }else if( n.getKind()==IFF || n.getKind()==XOR ){ + int depIndex1; + int eVal = evaluate( n[0], depIndex1, ri ); + if( eVal!=0 ){ + int depIndex2; + int eVal2 = evaluate( n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2, ri ); + if( eVal2!=0 ){ + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + return eVal==eVal2 ? 1 : -1; + } + } + return 0; + }else if( n.getKind()==ITE ){ + int depIndex1, depIndex2; + int eVal = evaluate( n[0], depIndex1, ri ); + if( eVal==0 ){ + //evaluate children to see if they are the same value + int eval1 = evaluate( n[1], depIndex1, ri ); + if( eval1!=0 ){ + int eval2 = evaluate( n[1], depIndex2, ri ); + if( eval1==eval2 ){ + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + return eval1; + } + } + }else{ + int eValT = evaluate( n[eVal==1 ? 1 : 2], depIndex2, ri ); + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + return eValT; + } + return 0; + }else if( n.getKind()==FORALL ){ + return 0; + }else{ + ++d_eval_lits; + ////if we know we will fail again, immediately return + //if( d_eval_failed.find( n )!=d_eval_failed.end() ){ + // if( d_eval_failed[n] ){ + // return -1; + // } + //} + //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl; + int retVal = 0; + depIndex = ri->getNumTerms()-1; + Node val = evaluateTerm( n, depIndex, ri ); + if( !val.isNull() ){ + if( areEqual( val, d_true ) ){ + retVal = 1; + }else if( areEqual( val, d_false ) ){ + retVal = -1; + }else{ + if( val.getKind()==EQUAL ){ + if( areEqual( val[0], val[1] ) ){ + retVal = 1; + }else if( areDisequal( val[0], val[1] ) ){ + retVal = -1; + } + } + } + } + if( retVal!=0 ){ + Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl; + }else{ + ++d_eval_lits_unknown; + Trace("fmf-eval-amb") << "Neither true nor false : " << n << std::endl; + Trace("fmf-eval-amb") << " value : " << val << std::endl; + //std::cout << "Neither true nor false : " << n << std::endl; + //std::cout << " Value : " << val << std::endl; + //for( int i=0; i<(int)n.getNumChildren(); i++ ){ + // std::cout << " " << i << " : " << n[i].getType() << std::endl; + //} + } + return retVal; + } +} + +Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){ + //Message() << "Eval term " << n << std::endl; + if( !n.hasAttribute(InstConstantAttribute()) ){ + //if evaluating a ground term, just consult the standard getValue functionality + depIndex = -1; + return getValue( n ); + }else{ + Node val; + depIndex = ri->getNumTerms()-1; + //check the type of n + if( n.getKind()==INST_CONSTANT ){ + int v = n.getAttribute(InstVarNumAttribute()); + depIndex = ri->d_var_order[ v ]; + val = ri->getTerm( v ); + }else if( n.getKind()==ITE ){ + int depIndex1, depIndex2; + int eval = evaluate( n[0], depIndex1, ri ); + if( eval==0 ){ + //evaluate children to see if they are the same + Node val1 = evaluateTerm( n[ 1 ], depIndex1, ri ); + Node val2 = evaluateTerm( n[ 2 ], depIndex2, ri ); + if( val1==val2 ){ + val = val1; + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + }else{ + return Node::null(); + } + }else{ + val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2, ri ); + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + } + }else{ + std::vector< int > children_depIndex; + //for select, pre-process read over writes + if( n.getKind()==SELECT ){ #if 0 - out << "---Current Model---" << std::endl; - out << "Representatives: " << std::endl; - d_rep_set.toStream( out ); - out << "Functions: " << std::endl; - for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){ - it->second.toStream( out ); - out << std::endl; + //std::cout << "Evaluate " << n << std::endl; + Node sel = evaluateTerm( n[1], depIndex, ri ); + if( sel.isNull() ){ + depIndex = ri->getNumTerms()-1; + return Node::null(); + } + Node arr = getRepresentative( n[0] ); + //if( n[0]!=getRepresentative( n[0] ) ){ + // std::cout << n[0] << " is " << getRepresentative( n[0] ) << std::endl; + //} + int tempIndex; + int eval = 1; + while( arr.getKind()==STORE && eval!=0 ){ + eval = evaluate( sel.eqNode( arr[1] ), tempIndex, ri ); + depIndex = tempIndex > depIndex ? tempIndex : depIndex; + if( eval==1 ){ + val = evaluateTerm( arr[2], tempIndex, ri ); + depIndex = tempIndex > depIndex ? tempIndex : depIndex; + return val; + }else if( eval==-1 ){ + arr = arr[0]; + } + } + arr = evaluateTerm( arr, tempIndex, ri ); + depIndex = tempIndex > depIndex ? tempIndex : depIndex; + val = NodeManager::currentNM()->mkNode( SELECT, arr, sel ); +#else + val = evaluateTermDefault( n, depIndex, children_depIndex, ri ); +#endif + }else{ + //default term evaluate : evaluate all children, recreate the value + val = evaluateTermDefault( n, depIndex, children_depIndex, ri ); + } + if( !val.isNull() ){ + bool setVal = false; + //custom ways of evaluating terms + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; + //if it is a defined UF, then consult the interpretation + if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){ + ++d_eval_uf_terms; + int argDepIndex = 0; + //make the term model specifically for n + makeEvalUfModel( n ); + //now, consult the model + if( d_eval_uf_use_default[n] ){ + val = d_uf_model_tree[ op ].getValue( this, val, argDepIndex ); + }else{ + val = d_eval_uf_model[ n ].getValue( this, val, argDepIndex ); + } + //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; + //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe ); + Assert( !val.isNull() ); + //recalculate the depIndex + depIndex = -1; + for( int i=0; i<argDepIndex; i++ ){ + int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i]; + Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl; + if( children_depIndex[index]>depIndex ){ + depIndex = children_depIndex[index]; + } + } + setVal = true; + } + }else if( n.getKind()==SELECT ){ + //we are free to interpret this term however we want + } + //if not set already, rewrite and consult model for interpretation + if( !setVal ){ + val = Rewriter::rewrite( val ); + if( val.getMetaKind()!=kind::metakind::CONSTANT ){ + //FIXME: we cannot do this until we trust all theories collectModelInfo! + //val = getInterpretedValue( val ); + //val = getRepresentative( val ); + } + } + Debug("fmf-eval-debug") << "Evaluate term " << n << " = "; + printRepresentativeDebug( "fmf-eval-debug", val ); + Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl; + } + } + return val; + } +} + +Node FirstOrderModel::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){ + depIndex = -1; + if( n.getNumChildren()==0 ){ + return n; + }else{ + //first we must evaluate the arguments + std::vector< Node > children; + if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + //for each argument, calculate its value, and the variables its value depends upon + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + childDepIndex.push_back( -1 ); + Node nn = evaluateTerm( n[i], childDepIndex[i], ri ); + if( nn.isNull() ){ + depIndex = ri->getNumTerms()-1; + return nn; + }else{ + children.push_back( nn ); + if( childDepIndex[i]>depIndex ){ + depIndex = childDepIndex[i]; + } + } + } + //recreate the value + Node val = NodeManager::currentNM()->mkNode( n.getKind(), children ); + return val; + } +} + +void FirstOrderModel::clearEvalFailed( int index ){ + for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){ + d_eval_failed[ d_eval_failed_lits[index][i] ] = false; + } + d_eval_failed_lits[index].clear(); +} + +void FirstOrderModel::makeEvalUfModel( Node n ){ + if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){ + makeEvalUfIndexOrder( n ); + if( !d_eval_uf_use_default[n] ){ + Node op = n.getOperator(); + d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] ); + d_uf_model_gen[op].makeModel( this, d_eval_uf_model[n] ); + //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl; + //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 ); + } } -#elif 0 - d_rep_set.toStream( out ); - //print everything not related to UF in equality engine - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - Node rep = getRepresentative( eqc ); - TypeNode type = rep.getType(); - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - //do not print things that have interpretations in model - if( !(*eqc_i).isConst() && !hasInterpretedValue( *eqc_i ) ){ - out << "(" << (*eqc_i) << " " << rep << ")" << std::endl; +} + +struct sortGetMaxVariableNum { + std::map< Node, int > d_max_var_num; + int computeMaxVariableNum( Node n ){ + if( n.getKind()==INST_CONSTANT ){ + return n.getAttribute(InstVarNumAttribute()); + }else if( n.hasAttribute(InstConstantAttribute()) ){ + int maxVal = -1; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + int val = getMaxVariableNum( n[i] ); + if( val>maxVal ){ + maxVal = val; + } } - ++eqc_i; + return maxVal; + }else{ + return -1; } - ++eqcs_i; } - //print functions - for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){ - it->second.toStream( out ); - out << std::endl; + int getMaxVariableNum( Node n ){ + std::map< Node, int >::iterator it = d_max_var_num.find( n ); + if( it==d_max_var_num.end() ){ + int num = computeMaxVariableNum( n ); + d_max_var_num[n] = num; + return num; + }else{ + return it->second; + } } + bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));} +}; + +void FirstOrderModel::makeEvalUfIndexOrder( Node n ){ + if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){ +#ifdef USE_INDEX_ORDERING + //sort arguments in order of least significant vs. most significant variable in default ordering + std::map< Node, std::vector< int > > argIndex; + std::vector< Node > args; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( argIndex.find( n[i] )==argIndex.end() ){ + args.push_back( n[i] ); + } + argIndex[n[i]].push_back( i ); + } + sortGetMaxVariableNum sgmvn; + std::sort( args.begin(), args.end(), sgmvn ); + for( int i=0; i<(int)args.size(); i++ ){ + for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){ + d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] ); + } + } + bool useDefault = true; + for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ + if( i!=d_eval_term_index_order[n][i] ){ + useDefault = false; + break; + } + } + d_eval_uf_use_default[n] = useDefault; + Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : "; + for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ + Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " "; + } + Debug("fmf-index-order") << std::endl; +#else + d_eval_uf_use_default[n] = true; #endif + } } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 8ad911452..e66bf8040 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -42,32 +42,41 @@ class TermDb; class FirstOrderModel : public DefaultModel { private: - //pointer to term database - TermDb* d_term_db; //add term function void addTerm( Node n ); //for initialize model void initializeModelForTerm( Node n ); - /** to stream functions */ - void toStreamFunction( Node n, std::ostream& out ); - void toStreamType( TypeNode tn, std::ostream& out ); + /** 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; public: //for Theory UF: //models for each UF operator std::map< Node, uf::UfModelTree > d_uf_model_tree; //model generators std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen; +private: + //map from terms to the models used to calculate their value + std::map< Node, bool > d_eval_uf_use_default; + std::map< Node, uf::UfModelTree > d_eval_uf_model; + void makeEvalUfModel( Node n ); + //index ordering to use for each term + std::map< Node, std::vector< int > > d_eval_term_index_order; + void makeEvalUfIndexOrder( Node n ); public: //for Theory Arrays: //default value for each non-store array std::map< Node, arrays::ArrayModel > d_array_model; public: //for Theory Quantifiers: - /** list of quantifiers asserted in the current context */ - context::CDList<Node> d_forall_asserts; + /** assert quantifier */ + void assertQuantifier( Node n ); /** get number of asserted quantifiers */ int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); } /** get asserted quantifier */ Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; } + /** bool axiom asserted */ + bool isAxiomAsserted() { return d_axiom_asserted; } public: - FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ); + FirstOrderModel( context::Context* c, std::string name ); virtual ~FirstOrderModel(){} // reset the model void reset(); @@ -75,11 +84,30 @@ public: Node getInterpretedValue( TNode n ); public: // initialize the model - void initialize(); - /** get term database */ - TermDb* getTermDatabase(); + void initialize( bool considerAxioms = true ); /** to stream function */ void toStream( std::ostream& out ); + +//the following functions are for evaluating quantifier bodies +public: + /** reset evaluation */ + void resetEvaluate(); + /** evaluate functions */ + int evaluate( Node n, int& depIndex, RepSetIterator* ri ); + Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ); +public: + //statistics + int d_eval_formulas; + int d_eval_uf_terms; + int d_eval_lits; + int d_eval_lits_unknown; +private: + //default evaluate term function + Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ); + //temporary storing which literals have failed + void clearEvalFailed( int index ); + std::map< Node, bool > d_eval_failed; + std::map< int, std::vector< Node > > d_eval_failed_lits; };/* class FirstOrderModel */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index ce35607d4..d2083ef3d 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -148,7 +148,9 @@ void InstMatch::computeTermVec( QuantifiersEngine* qe, const std::vector< Node > } void InstMatch::computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match ){ for( int i=0; i<(int)vars.size(); i++ ){ - match.push_back( d_map[ vars[i] ] ); + if( d_map.find( vars[i] )!=d_map.end() && !d_map[ vars[i] ].isNull() ){ + match.push_back( d_map[ vars[i] ] ); + } } } @@ -177,7 +179,7 @@ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m } if( modEq ){ //check modulo equality if any other instantiation match exists - if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ + if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ), qe->getEqualityQuery()->getEngine() ); while( !eqc.isFinished() ){ @@ -193,13 +195,6 @@ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m ++eqc; } } - //for( std::map< Node, InstMatchTrie >::iterator itc = d_data.begin(); itc != d_data.end(); ++itc ){ - // if( itc->first!=n && qe->getEqualityQuery()->areEqual( n, itc->first ) ){ - // if( itc->second.existsInstMatch( qe, f, m, modEq, index+1 ) ){ - // return true; - // } - // } - //} } return false; } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 0fa4fad12..727f568c5 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -386,3 +386,16 @@ void InstantiationEngine::propagate( Theory::Effort level ){ } } } + +Node InstantiationEngine::getNextDecisionRequest(){ + //propagate as decision all counterexample literals that are not asserted + for( std::map< Node, Node >::iterator it = d_ce_lit.begin(); it != d_ce_lit.end(); ++it ){ + bool value; + if( !d_quantEngine->getValuation().hasSatValue( it->second, value ) ){ + //if not already set, propagate as decision + Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << it->second << std::endl; + return it->second; + } + } + return Node::null(); +}
\ No newline at end of file diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 37ee6d801..19dac736c 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -66,6 +66,7 @@ public: void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } void propagate( Theory::Effort level ); + Node getNextDecisionRequest(); public: /** get the corresponding counterexample literal for quantified formula node n */ Node getCounterexampleLiteralFor( Node f ) { return d_ce_lit.find( f )==d_ce_lit.end() ? Node::null() : d_ce_lit[ f ]; } diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index 106d95cef..c81816528 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -8,7 +8,7 @@ theory THEORY_QUANTIFIERS ::CVC4::theory::quantifiers::TheoryQuantifiers "theory typechecker "theory/quantifiers/theory_quantifiers_type_rules.h" instantiator ::CVC4::theory::quantifiers::InstantiatorTheoryQuantifiers "theory/quantifiers/theory_quantifiers_instantiator.h" -properties check propagate presolve +properties check propagate presolve getNextDecisionRequest rewriter ::CVC4::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h" @@ -30,6 +30,9 @@ sort INST_PATTERN_TYPE \ not-well-founded \ "Instantiation pattern type" +# Instantiation pattern, also called trigger. +# This node is used for specifying hints for quantifier instantiation. +# An instantiation pattern may have more than 1 child, in which case it specifies a multi-trigger. operator INST_PATTERN 1: "instantiation pattern" sort INST_PATTERN_LIST_TYPE \ @@ -37,6 +40,7 @@ sort INST_PATTERN_LIST_TYPE \ not-well-founded \ "Instantiation pattern list type" +# a list of instantiation patterns operator INST_PATTERN_LIST 1: "instantiation pattern list" typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule diff --git a/src/theory/quantifiers/literal_match_mode.cpp b/src/theory/quantifiers/literal_match_mode.cpp deleted file mode 100644 index 87b4b94fe..000000000 --- a/src/theory/quantifiers/literal_match_mode.cpp +++ /dev/null @@ -1,43 +0,0 @@ -/********************* */ -/*! \file literal_match_mode.cpp - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include <iostream> -#include "theory/quantifiers/literal_match_mode.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) { - switch(mode) { - case theory::quantifiers::LITERAL_MATCH_NONE: - out << "LITERAL_MATCH_NONE"; - break; - case theory::quantifiers::LITERAL_MATCH_PREDICATE: - out << "LITERAL_MATCH_PREDICATE"; - break; - case theory::quantifiers::LITERAL_MATCH_EQUALITY: - out << "LITERAL_MATCH_EQUALITY"; - break; - default: - out << "LiteralMatchMode!UNKNOWN"; - } - - return out; -} - -}/* CVC4 namespace */ diff --git a/src/theory/quantifiers/literal_match_mode.h b/src/theory/quantifiers/literal_match_mode.h deleted file mode 100644 index 189f0a235..000000000 --- a/src/theory/quantifiers/literal_match_mode.h +++ /dev/null @@ -1,47 +0,0 @@ -/********************* */ -/*! \file literal_match_mode.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H -#define __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H - -#include <iostream> - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -typedef enum { - /** Do not consider polarity of patterns */ - LITERAL_MATCH_NONE, - /** Consider polarity of boolean predicates only */ - LITERAL_MATCH_PREDICATE, - /** Consider polarity of boolean predicates, as well as equalities */ - LITERAL_MATCH_EQUALITY, -} LiteralMatchMode; - -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H */ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 5d49c914f..c09346f35 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -20,15 +20,14 @@ #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_model.h" #include "theory/uf/theory_uf_instantiator.h" +#include "theory/uf/theory_uf_strong_solver.h" #include "theory/arrays/theory_arrays_model.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/model_builder.h" - -//#define ME_PRINT_WARNINGS +#include "theory/quantifiers/quantifiers_attributes.h" #define RECONSIDER_FUNC_CONSTANT -//#define ONE_QUANT_PER_ROUND_INST_GEN using namespace std; using namespace CVC4; @@ -37,78 +36,95 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -ModelEngineBuilder::ModelEngineBuilder( QuantifiersEngine* qe ) : +ModelEngineBuilder::ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe ) : TheoryEngineModelBuilder( qe->getTheoryEngine() ), -d_qe( qe ){ - +d_qe( qe ), d_curr_model( c, NULL ){ + d_considerAxioms = true; } -Node ModelEngineBuilder::chooseRepresentative( TheoryModel* m, Node eqc ){ - Assert( m->d_equalityEngine.hasTerm( eqc ) ); - Assert( m->d_equalityEngine.getRepresentative( eqc )==eqc ); - //avoid interpreted symbols - if( isBadRepresentative( eqc ) ){ - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &m->d_equalityEngine ); - while( !eqc_i.isFinished() ){ - if( !isBadRepresentative( *eqc_i ) ){ - return *eqc_i; +Node ModelEngineBuilder::chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ){ + if( fullModel ){ + return TheoryEngineModelBuilder::chooseRepresentative( m, eqc, fullModel ); + }else{ + Assert( m->d_equalityEngine.hasTerm( eqc ) ); + Assert( m->d_equalityEngine.getRepresentative( eqc )==eqc ); + //avoid bad representatives + if( isBadRepresentative( eqc ) ){ + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &m->d_equalityEngine ); + while( !eqc_i.isFinished() ){ + if( !isBadRepresentative( *eqc_i ) ){ + return *eqc_i; + } + ++eqc_i; } - ++eqc_i; + //otherwise, make new value? + //Message() << "Warning: Bad rep " << eqc << std::endl; } - //otherwise, make new value? - //Message() << "Warning: Bad rep " << eqc << std::endl; + return eqc; } - return eqc; } bool ModelEngineBuilder::isBadRepresentative( Node n ){ + //avoid interpreted symbols return n.getKind()==SELECT || n.getKind()==APPLY_SELECTOR; } -void ModelEngineBuilder::processBuildModel( TheoryModel* m ) { - d_addedLemmas = 0; - //only construct first order model if optUseModel() is true - if( optUseModel() ){ - FirstOrderModel* fm = (FirstOrderModel*)m; - //initialize model - fm->initialize(); - //analyze the functions - analyzeModel( fm ); - //analyze the quantifiers - Debug("fmf-model-debug") << "Analyzing quantifiers..." << std::endl; - analyzeQuantifiers( fm ); - //if applicable, find exceptions - if( optInstGen() ){ - //now, see if we know that any exceptions via InstGen exist - Debug("fmf-model-debug") << "Perform InstGen techniques for quantifiers..." << std::endl; - for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - if( d_quant_sat.find( f )==d_quant_sat.end() ){ - d_addedLemmas += doInstGen( fm, f ); - if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){ - break; +void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { + FirstOrderModel* fm = (FirstOrderModel*)m; + if( fullModel ){ + Assert( d_curr_model==fm ); + //update models + for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ + it->second.update( fm ); + } + + }else{ + d_curr_model = fm; + //build model for relevant symbols contained in quantified formulas + d_addedLemmas = 0; + //only construct first order model if optUseModel() is true + if( optUseModel() ){ + //initialize model + fm->initialize( d_considerAxioms ); + //analyze the functions + Trace("model-engine-debug") << "Analyzing model..." << std::endl; + analyzeModel( fm ); + //analyze the quantifiers + Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl; + analyzeQuantifiers( fm ); + //if applicable, find exceptions + if( optInstGen() ){ + //now, see if we know that any exceptions via InstGen exist + Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl; + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + if( isQuantifierActive( f ) ){ + d_addedLemmas += doInstGen( fm, f ); + if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){ + break; + } } } - } - if( Trace.isOn("model-engine") ){ - if( d_addedLemmas>0 ){ - Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl; - }else{ - Trace("model-engine") << "No InstGen lemmas..." << std::endl; + if( Trace.isOn("model-engine") ){ + if( d_addedLemmas>0 ){ + Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl; + }else{ + Trace("model-engine") << "No InstGen lemmas..." << std::endl; + } } } - Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl; - } - if( d_addedLemmas==0 ){ - //if no immediate exceptions, build the model - // this model will be an approximation that will need to be tested via exhaustive instantiation - Debug("fmf-model-debug") << "Building model..." << std::endl; - finishBuildModel( fm ); + if( d_addedLemmas==0 ){ + //if no immediate exceptions, build the model + // this model will be an approximation that will need to be tested via exhaustive instantiation + Trace("model-engine-debug") << "Building model..." << std::endl; + constructModel( fm ); + } } } } void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ + d_uf_model_constructed.clear(); //determine if any functions are constant for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ Node op = it->first; @@ -138,108 +154,138 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ } void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){ - d_quant_selection_lits.clear(); d_quant_sat.clear(); + d_quant_selection_lit.clear(); + d_quant_selection_lit_candidates.clear(); + d_quant_selection_lit_terms.clear(); + d_term_selection_lit.clear(); + d_op_selection_terms.clear(); d_uf_prefs.clear(); int quantSatInit = 0; int nquantSatInit = 0; //analyze the preferences of each quantifier for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); - Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; - std::vector< Node > pro_con[2]; - std::vector< Node > constantSatOps; - bool constantSatReconsider; - //for each asserted quantifier f, - // - determine which literals form model basis for each quantifier - // - check which function/predicates have good and bad definitions according to f - for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin(); - it != d_qe->d_phase_reqs[f].end(); ++it ){ - Node n = it->first; - Node gn = d_qe->getTermDatabase()->getModelBasis( n ); - Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl; - //calculate preference - int pref = 0; - bool value; - if( d_qe->getValuation().hasSatValue( gn, value ) ){ - if( value!=it->second ){ - //store this literal as a model basis literal - // this literal will force a default values in model that (modulo exceptions) shows - // that f is satisfied by the model - d_quant_selection_lits[f].push_back( value ? n : n.notNode() ); - pref = 1; - }else{ - pref = -1; - } - } - if( pref!=0 ){ - //Store preferences for UF - bool isConst = !n.hasAttribute(InstConstantAttribute()); - std::vector< Node > uf_terms; - if( gn.getKind()==APPLY_UF ){ - uf_terms.push_back( gn ); - isConst = !d_uf_prefs[gn.getOperator()].d_const_val.isNull(); - }else if( gn.getKind()==EQUAL ){ - isConst = true; - for( int j=0; j<2; j++ ){ - if( n[j].hasAttribute(InstConstantAttribute()) ){ - if( n[j].getKind()==APPLY_UF ){ - Node op = gn[j].getOperator(); - if( fm->d_uf_model_tree.find( op )!=fm->d_uf_model_tree.end() ){ - uf_terms.push_back( gn[j] ); - isConst = isConst && !d_uf_prefs[op].d_const_val.isNull(); - }else{ - isConst = false; + if( isQuantifierActive( f ) ){ + Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; + //the pro/con preferences for this quantifier + std::vector< Node > pro_con[2]; + //the terms in the selection literal we choose + std::vector< Node > selectionLitTerms; + //for each asserted quantifier f, + // - determine selection literals + // - check which function/predicates have good and bad definitions for satisfying f + for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin(); + it != d_qe->d_phase_reqs[f].end(); ++it ){ + //the literal n is phase-required for quantifier f + Node n = it->first; + Node gn = d_qe->getTermDatabase()->getModelBasis( n ); + Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl; + bool value; + //if the corresponding ground abstraction literal has a SAT value + if( d_qe->getValuation().hasSatValue( gn, value ) ){ + //collect the non-ground uf terms that this literal contains + // and compute if all of the symbols in this literal have + // constant definitions. + bool isConst = true; + std::vector< Node > uf_terms; + if( n.hasAttribute(InstConstantAttribute()) ){ + isConst = false; + if( gn.getKind()==APPLY_UF ){ + uf_terms.push_back( gn ); + isConst = !d_uf_prefs[gn.getOperator()].d_const_val.isNull(); + }else if( gn.getKind()==EQUAL ){ + isConst = true; + for( int j=0; j<2; j++ ){ + if( n[j].hasAttribute(InstConstantAttribute()) ){ + if( n[j].getKind()==APPLY_UF && + fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){ + uf_terms.push_back( gn[j] ); + isConst = isConst && !d_uf_prefs[ gn[j].getOperator() ].d_const_val.isNull(); + }else{ + isConst = false; + } } - }else{ - isConst = false; } } } - } - Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" ); - Debug("fmf-model-prefs") << " the definition of " << n << std::endl; - if( pref==1 && isConst ){ - d_quant_sat[f] = true; - //instead, just note to the model for each uf term that f is pro its definition - constantSatReconsider = false; - constantSatOps.clear(); - for( int j=0; j<(int)uf_terms.size(); j++ ){ - Node op = uf_terms[j].getOperator(); - constantSatOps.push_back( op ); - if( d_uf_prefs[op].d_reconsiderModel ){ - constantSatReconsider = true; + //check if the value in the SAT solver matches the preference according to the quantifier + int pref = 0; + if( value!=it->second ){ + //we have a possible selection literal + bool selectLit = d_quant_selection_lit[f].isNull(); + bool selectLitConstraints = true; + //it is a constantly defined selection literal : the quantifier is sat + if( isConst ){ + selectLit = selectLit || d_quant_sat.find( f )==d_quant_sat.end(); + d_quant_sat[f] = true; + //check if choosing this literal would add any additional constraints to default definitions + selectLitConstraints = false; + for( int j=0; j<(int)uf_terms.size(); j++ ){ + Node op = uf_terms[j].getOperator(); + if( d_uf_prefs[op].d_reconsiderModel ){ + selectLitConstraints = true; + } + } + if( !selectLitConstraints ){ + selectLit = true; + } } + //see if we wish to choose this as a selection literal + d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() ); + if( selectLit ){ + Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl; + d_quant_selection_lit[f] = value ? n : n.notNode(); + selectionLitTerms.clear(); + selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() ); + if( !selectLitConstraints ){ + break; + } + } + pref = 1; + }else{ + pref = -1; } - if( !constantSatReconsider ){ - break; - } - }else{ - int pcIndex = pref==1 ? 0 : 1; - for( int j=0; j<(int)uf_terms.size(); j++ ){ - pro_con[pcIndex].push_back( uf_terms[j] ); + //if we are not yet SAT, so we will add to preferences + if( d_quant_sat.find( f )==d_quant_sat.end() ){ + Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" ); + Debug("fmf-model-prefs") << " the definition of " << n << std::endl; + for( int j=0; j<(int)uf_terms.size(); j++ ){ + pro_con[ pref==1 ? 0 : 1 ].push_back( uf_terms[j] ); + } } } } - } - if( d_quant_sat.find( f )!=d_quant_sat.end() ){ - Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: "; - for( int i=0; i<(int)constantSatOps.size(); i++ ){ - Debug("fmf-model-prefs") << constantSatOps[i] << " "; - d_uf_prefs[constantSatOps[i]].d_reconsiderModel = false; + //process information about selection literal for f + if( !d_quant_selection_lit[f].isNull() ){ + d_quant_selection_lit_terms[f].insert( d_quant_selection_lit_terms[f].begin(), selectionLitTerms.begin(), selectionLitTerms.end() ); + for( int i=0; i<(int)selectionLitTerms.size(); i++ ){ + d_term_selection_lit[ selectionLitTerms[i] ] = d_quant_selection_lit[f]; + d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] ); + } + }else{ + Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals (is the body of f clausified?)" << std::endl; } - Debug("fmf-model-prefs") << std::endl; - quantSatInit++; - d_statistics.d_pre_sat_quant += quantSatInit; - }else{ - nquantSatInit++; - d_statistics.d_pre_nsat_quant += quantSatInit; - //note quantifier's value preferences to models - for( int k=0; k<2; k++ ){ - for( int j=0; j<(int)pro_con[k].size(); j++ ){ - Node op = pro_con[k][j].getOperator(); - Node r = fm->getRepresentative( pro_con[k][j] ); - d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 ); + //process information about requirements and preferences of quantifier f + if( d_quant_sat.find( f )!=d_quant_sat.end() ){ + Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: "; + for( int i=0; i<(int)selectionLitTerms.size(); i++ ){ + Debug("fmf-model-prefs") << selectionLitTerms[i] << " "; + d_uf_prefs[ selectionLitTerms[i].getOperator() ].d_reconsiderModel = false; + } + Debug("fmf-model-prefs") << std::endl; + quantSatInit++; + ++(d_statistics.d_pre_sat_quant); + }else{ + nquantSatInit++; + ++(d_statistics.d_pre_nsat_quant); + //note quantifier's value preferences to models + for( int k=0; k<2; k++ ){ + for( int j=0; j<(int)pro_con[k].size(); j++ ){ + Node op = pro_con[k][j].getOperator(); + Node r = fm->getRepresentative( pro_con[k][j] ); + d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 ); + } } } } @@ -248,58 +294,87 @@ void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){ } int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){ - //we wish to add all known exceptions to our model basis literal(s) - // this will help to refine our current model. + int addedLemmas = 0; + //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model. //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms, // effectively acting as partial instantiations instead of pointwise instantiations. - int addedLemmas = 0; - for( int i=0; i<(int)d_quant_selection_lits[f].size(); i++ ){ - bool phase = d_quant_selection_lits[f][i].getKind()!=NOT; - Node lit = d_quant_selection_lits[f][i].getKind()==NOT ? d_quant_selection_lits[f][i][0] : d_quant_selection_lits[f][i]; + if( !d_quant_selection_lit[f].isNull() ){ +#if 0 + bool phase = d_quant_selection_lit[f].getKind()!=NOT; + Node lit = d_quant_selection_lit[f].getKind()==NOT ? d_quant_selection_lit[f][0] : d_quant_selection_lit[f]; Assert( lit.hasAttribute(InstConstantAttribute()) ); - std::vector< Node > tr_terms; - if( lit.getKind()==APPLY_UF ){ - //only match predicates that are contrary to this one, use literal matching - Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); - fm->getTermDatabase()->setInstantiationConstantAttr( eq, f ); - tr_terms.push_back( eq ); - }else if( lit.getKind()==EQUAL ){ - //collect trigger terms - for( int j=0; j<2; j++ ){ - if( lit[j].hasAttribute(InstConstantAttribute()) ){ - if( lit[j].getKind()==APPLY_UF ){ - tr_terms.push_back( lit[j] ); - }else{ - tr_terms.clear(); - break; - } + for( size_t i=0; i<d_quant_selection_lit_terms[f].size(); i++ ){ + Node n1 = d_quant_selection_lit_terms[f][i]; + Node op = d_quant_selection_lit_terms[f][i].getOperator(); + //check all other selection literals involving "op" + for( size_t i=0; i<d_op_selection_terms[op].size(); i++ ){ + Node n2 = d_op_selection_terms[op][i]; + Node n2_lit = d_term_selection_lit[ n2 ]; + if( n2_lit!=d_quant_selection_lit[f] ){ + //match n1 and n2 } } - if( tr_terms.size()==1 && !phase ){ - //equality between a function and a ground term, use literal matching - tr_terms.clear(); - tr_terms.push_back( lit ); + if( addedLemmas==0 ){ + //check all ground terms involving "op" + for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ + Node n2 = fm->d_uf_terms[op][i]; + if( n1!=n2 ){ + //match n1 and n2 + } + } } } - //if applicable, try to add exceptions here - if( !tr_terms.empty() ){ - //make a trigger for these terms, add instantiations - inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms ); - //Notice() << "Trigger = " << (*tr) << std::endl; - tr->resetInstantiationRound(); - tr->reset( Node::null() ); - //d_qe->d_optInstMakeRepresentative = false; - //d_qe->d_optMatchIgnoreModelBasis = true; - addedLemmas += tr->addInstantiations( d_quant_basis_match[f] ); +#else + Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl; + for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){ + bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT; + Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i]; + Assert( lit.hasAttribute(InstConstantAttribute()) ); + std::vector< Node > tr_terms; + if( lit.getKind()==APPLY_UF ){ + //only match predicates that are contrary to this one, use literal matching + Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); + d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f ); + tr_terms.push_back( eq ); + }else if( lit.getKind()==EQUAL ){ + //collect trigger terms + for( int j=0; j<2; j++ ){ + if( lit[j].hasAttribute(InstConstantAttribute()) ){ + if( lit[j].getKind()==APPLY_UF ){ + tr_terms.push_back( lit[j] ); + }else{ + tr_terms.clear(); + break; + } + } + } + if( tr_terms.size()==1 && !phase ){ + //equality between a function and a ground term, use literal matching + tr_terms.clear(); + tr_terms.push_back( lit ); + } + } + //if applicable, try to add exceptions here + if( !tr_terms.empty() ){ + //make a trigger for these terms, add instantiations + inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms ); + //Notice() << "Trigger = " << (*tr) << std::endl; + tr->resetInstantiationRound(); + tr->reset( Node::null() ); + //d_qe->d_optInstMakeRepresentative = false; + //d_qe->d_optMatchIgnoreModelBasis = true; + addedLemmas += tr->addInstantiations( d_quant_basis_match[f] ); + } } +#endif } return addedLemmas; } -void ModelEngineBuilder::finishBuildModel( FirstOrderModel* fm ){ +void ModelEngineBuilder::constructModel( FirstOrderModel* fm ){ //build model for UF for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ - finishBuildModelUf( fm, it->first ); + constructModelUf( fm, it->first ); } /* //build model for arrays @@ -311,10 +386,10 @@ void ModelEngineBuilder::finishBuildModel( FirstOrderModel* fm ){ it->second.setDefaultValue( fm->getRepresentative( selModelBasis ) ); } */ - Debug("fmf-model-debug") << "Done building models." << std::endl; + Trace("model-engine-debug") << "Done building models." << std::endl; } -void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, Node op ){ +void ModelEngineBuilder::constructModelUf( FirstOrderModel* fm, Node op ){ #ifdef RECONSIDER_FUNC_CONSTANT if( d_uf_model_constructed[op] ){ if( d_uf_prefs[op].d_reconsiderModel ){ @@ -337,7 +412,7 @@ void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, Node op ){ //set the values in the model for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ Node n = fm->d_uf_terms[op][i]; - fm->getTermDatabase()->computeModelBasisArgAttribute( n ); + d_qe->getTermDatabase()->computeModelBasisArgAttribute( n ); if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ Node v = fm->getRepresentative( n ); //if this assertion did not help the model, just consider it ground @@ -381,12 +456,6 @@ void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, Node op ){ } } -void ModelEngineBuilder::finishProcessBuildModel( TheoryModel* m ){ - for( std::map< Node, Node >::iterator it = m->d_reps.begin(); it != m->d_reps.end(); ++it ){ - //build proper representatives (TODO) - } -} - bool ModelEngineBuilder::optUseModel() { return options::fmfModelBasedInst(); } @@ -396,11 +465,11 @@ bool ModelEngineBuilder::optInstGen(){ } bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ -#ifdef ONE_QUANT_PER_ROUND_INST_GEN - return true; -#else - return false; -#endif + return options::fmfInstGenOneQuantPerRound(); +} + +void ModelEngineBuilder::setEffort( int effort ){ + d_considerAxioms = effort>=1; } ModelEngineBuilder::Statistics::Statistics(): @@ -415,3 +484,7 @@ ModelEngineBuilder::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_pre_sat_quant); StatisticsRegistry::unregisterStat(&d_pre_nsat_quant); } + +bool ModelEngineBuilder::isQuantifierActive( Node f ){ + return ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end(); +} diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 344b731e0..1366a7650 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -27,20 +27,29 @@ namespace CVC4 { namespace theory { namespace quantifiers { -//the model builder +/** model builder class + * This class is capable of building candidate models based on the current quantified formulas + * that are asserted. Use: + * (1) call ModelEngineBuilder::buildModel( m, false );, where m is a FirstOrderModel + * (2) if candidate model is determined to be a real model, + then call ModelEngineBuilder::buildModel( m, true ); + */ class ModelEngineBuilder : public TheoryEngineModelBuilder { protected: //quantifiers engine QuantifiersEngine* d_qe; + //the model we are working with + context::CDO< FirstOrderModel* > d_curr_model; //map from operators to model preference data std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; //built model uf std::map< Node, bool > d_uf_model_constructed; +protected: /** process build model */ - void processBuildModel( TheoryModel* m ); + void processBuildModel( TheoryModel* m, bool fullModel ); /** choose representative for unconstrained equivalence class */ - Node chooseRepresentative( TheoryModel* m, Node eqc ); + Node chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ); /** bad representative */ bool isBadRepresentative( Node n ); protected: @@ -49,23 +58,30 @@ protected: //analyze quantifiers void analyzeQuantifiers( FirstOrderModel* fm ); //build model - void finishBuildModel( FirstOrderModel* fm ); + void constructModel( FirstOrderModel* fm ); //theory-specific build models - void finishBuildModelUf( FirstOrderModel* fm, Node op ); + void constructModelUf( FirstOrderModel* fm, Node op ); //do InstGen techniques for quantifier, return number of lemmas produced int doInstGen( FirstOrderModel* fm, Node f ); public: - ModelEngineBuilder( QuantifiersEngine* qe ); + ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe ); virtual ~ModelEngineBuilder(){} - /** finish model */ - void finishProcessBuildModel( TheoryModel* m ); -public: /** number of lemmas generated while building model */ int d_addedLemmas; + //consider axioms + bool d_considerAxioms; +private: ///information for InstGen //map from quantifiers to if are constant SAT std::map< Node, bool > d_quant_sat; - //map from quantifiers to the instantiation literals that their model is dependent upon - std::map< Node, std::vector< Node > > d_quant_selection_lits; + //map from quantifiers to their selection literals + std::map< Node, Node > d_quant_selection_lit; + std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates; + //map from quantifiers to their selection literal terms + std::map< Node, std::vector< Node > > d_quant_selection_lit_terms; + //map from terms to the selection literals they exist in + std::map< Node, Node > d_term_selection_lit; + //map from operators to terms that appear in selection literals + std::map< Node, std::vector< Node > > d_op_selection_terms; public: //map from quantifiers to model basis match std::map< Node, InstMatch > d_quant_basis_match; @@ -73,6 +89,8 @@ public: bool optUseModel(); bool optInstGen(); bool optOneQuantPerRoundInstGen(); + // set effort + void setEffort( int effort ); /** statistics class */ class Statistics { public: @@ -82,6 +100,8 @@ public: ~Statistics(); }; Statistics d_statistics; + // is quantifier active? + bool isQuantifierActive( Node f ); };/* class ModelEngineBuilder */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index cbeeed8d0..b5a9ee74c 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -15,7 +15,6 @@ **/ #include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/rep_set_iterator.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" @@ -25,11 +24,11 @@ #include "theory/arrays/theory_arrays_model.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/quantifiers_attributes.h" //#define ME_PRINT_WARNINGS #define EVAL_FAIL_SKIP_MULTIPLE -//#define ONE_QUANT_PER_ROUND using namespace std; using namespace CVC4; @@ -40,96 +39,97 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; //Model Engine constructor -ModelEngine::ModelEngine( QuantifiersEngine* qe ) : +ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule( qe ), -d_builder( qe ), -d_rel_domain( qe->getModel() ){ +d_builder( c, qe ), +d_rel_domain( qe, qe->getModel() ){ } void ModelEngine::check( Theory::Effort e ){ if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){ - //first, check if we can minimize the model further - if( !((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){ - return; - } + FirstOrderModel* fm = d_quantEngine->getModel(); //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers int addedLemmas = 0; + Trace("model-engine") << "---Model Engine Round---" << std::endl; if( d_builder.optUseModel() ){ //check if any quantifiers are un-initialized - for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); addedLemmas += initializeQuantifier( f ); } } - if( addedLemmas==0 ){ - //quantifiers are initialized, we begin an instantiation round - double clSet = 0; - if( Trace.isOn("model-engine") ){ - clSet = double(clock())/double(CLOCKS_PER_SEC); - Trace("model-engine") << "---Model Engine Round---" << std::endl; - } - Debug("fmf-model-debug") << "---Begin Instantiation Round---" << std::endl; - ++(d_statistics.d_inst_rounds); - //reset the quantifiers engine - d_quantEngine->resetInstantiationRound( e ); - //initialize the model - Debug("fmf-model-debug") << "Build model..." << std::endl; - d_builder.buildModel( d_quantEngine->getModel() ); - d_quantEngine->d_model_set = true; - //if builder has lemmas, add and return - if( d_builder.d_addedLemmas>0 ){ - addedLemmas += (int)d_builder.d_addedLemmas; - }else{ - //print debug - Debug("fmf-model-complete") << std::endl; - debugPrint("fmf-model-complete"); - //verify we are SAT by trying exhaustive instantiation - if( optUseRelevantDomain() ){ - d_rel_domain.compute(); + if( addedLemmas>0 ){ + Trace("model-engine") << "Initialize, Added Lemmas = " << addedLemmas << std::endl; + } + //two effort levels: first try exhaustive instantiation without axioms, then with. + int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; + for( int effort=startEffort; effort<2; effort++ ){ + // for effort = 0, we only instantiate non-axioms + // for effort = 1, we instantiate everything + if( addedLemmas==0 ){ + //quantifiers are initialized, we begin an instantiation round + double clSet = 0; + if( Trace.isOn("model-engine") ){ + clSet = double(clock())/double(CLOCKS_PER_SEC); } - d_triedLemmas = 0; - d_testLemmas = 0; - d_relevantLemmas = 0; - d_totalLemmas = 0; - Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl; - for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( d_builder.d_quant_sat.find( f )==d_builder.d_quant_sat.end() ){ - addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() ); - if( optOneQuantPerRound() && addedLemmas>0 ){ - break; - } - } -#ifdef ME_PRINT_WARNINGS - if( addedLemmas>10000 ){ - break; + ++(d_statistics.d_inst_rounds); + //reset the quantifiers engine + d_quantEngine->resetInstantiationRound( e ); + //initialize the model + Trace("model-engine-debug") << "Build model..." << std::endl; + d_builder.setEffort( effort ); + d_builder.buildModel( fm, false ); + //if builder has lemmas, add and return + if( d_builder.d_addedLemmas>0 ){ + addedLemmas += (int)d_builder.d_addedLemmas; + }else{ + Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; + //let the strong solver verify that the model is minimal + uf::StrongSolverTheoryUf* uf_ss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver(); + //for debugging, this will if there are terms in the model that the strong solver was not notified of + uf_ss->debugModel( fm ); + Trace("model-engine-debug") << "Check model..." << std::endl; + //print debug + Debug("fmf-model-complete") << std::endl; + debugPrint("fmf-model-complete"); + //successfully built an acceptable model, now check it + checkModel( addedLemmas ); + //print debug information + if( Trace.isOn("model-engine") ){ + Trace("model-engine") << "Instantiate axioms : " << ( d_builder.d_considerAxioms ? "yes" : "no" ) << std::endl; + Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; + Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; } -#endif - } - Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; - Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; - if( Trace.isOn("model-engine") ){ - Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; - Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; - double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; } -#ifdef ME_PRINT_WARNINGS - if( addedLemmas>10000 ){ - Debug("fmf-exit") << std::endl; - debugPrint("fmf-exit"); - exit( 0 ); + } + if( addedLemmas==0 ){ + //if we have not added lemmas yet and axiomInstMode=trust, then we are done + if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){ + //we must return unknown if an axiom is asserted + if( effort==0 ){ + d_incomplete_check = true; + } + break; } -#endif } } if( addedLemmas==0 ){ - //CVC4 will answer SAT - Debug("fmf-consistent") << std::endl; + Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl; + //CVC4 will answer SAT or unknown + Trace("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); - // finish building the model in the standard way - d_builder.finishProcessBuildModel( d_quantEngine->getModel() ); + if( options::produceModels() ){ + // finish building the model in the standard way + d_builder.buildModel( fm, true ); + d_quantEngine->d_model_set = true; + } + //if the check was incomplete, we must set incomplete flag + if( d_incomplete_check ){ + d_quantEngine->getOutputChannel().setIncomplete(); + } }else{ //otherwise, the search will continue d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); @@ -154,11 +154,7 @@ bool ModelEngine::optUseRelevantDomain(){ } bool ModelEngine::optOneQuantPerRound(){ -#ifdef ONE_QUANT_PER_ROUND - return true; -#else - return false; -#endif + return options::fmfOneQuantPerRound(); } int ModelEngine::initializeQuantifier( Node f ){ @@ -178,11 +174,13 @@ int ModelEngine::initializeQuantifier( Node f ){ // Notice() << "Unhandled phase req: " << n << std::endl; // } //} + std::vector< Node > vars; std::vector< Node > ics; std::vector< Node > terms; for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); Node t = d_quantEngine->getTermDatabase()->getModelBasisTerm( ic.getType() ); + vars.push_back( f[0][j] ); ics.push_back( ic ); terms.push_back( t ); //calculate the basis match for f @@ -193,67 +191,137 @@ int ModelEngine::initializeQuantifier( Node f ){ Node n = d_quantEngine->getTermDatabase()->getCounterexampleBody( f ); Node gn = n.substitute( ics.begin(), ics.end(), terms.begin(), terms.end() ); d_quantEngine->getTermDatabase()->registerModelBasis( n, gn ); - //add model basis instantiation - if( d_quantEngine->addInstantiation( f, terms ) ){ - return 1; - }else{ - //shouldn't happen usually, but will occur if x != y is a required literal for f. - //Notice() << "No model basis for " << f << std::endl; - ++(d_statistics.d_num_quants_init_fail); + if( d_builder.optInstGen() ){ + //add model basis instantiation + if( d_quantEngine->addInstantiation( f, vars, terms ) ){ + return 1; + }else{ + //shouldn't happen usually, but will occur if x != y is a required literal for f. + //Notice() << "No model basis for " << f << std::endl; + ++(d_statistics.d_num_quants_init_fail); + } } } return 0; } -int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ - int tests = 0; - int addedLemmas = 0; - int triedLemmas = 0; - Debug("inst-fmf-ei") << "Add matches for " << f << "..." << std::endl; - Debug("inst-fmf-ei") << " Instantiation Constants: "; - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; +void ModelEngine::checkModel( int& addedLemmas ){ + FirstOrderModel* fm = d_quantEngine->getModel(); + //for debugging + if( Trace.isOn("model-engine") ){ + for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); it != fm->d_rep_set.d_type_reps.end(); ++it ){ + if( it->first.isSort() ){ + Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; + Trace("model-engine-debug") << " "; + for( size_t i=0; i<it->second.size(); i++ ){ + Trace("model-engine-debug") << it->second[i] << " "; + } + Trace("model-engine-debug") << std::endl; + } + } + } + //verify we are SAT by trying exhaustive instantiation + d_incomplete_check = false; + if( optUseRelevantDomain() ){ + d_rel_domain.compute(); } - Debug("inst-fmf-ei") << std::endl; - if( d_builder.d_quant_selection_lits[f].empty() ){ - Debug("inst-fmf-ei") << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl; + d_triedLemmas = 0; + d_testLemmas = 0; + d_relevantLemmas = 0; + d_totalLemmas = 0; + Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl; + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() ); #ifdef ME_PRINT_WARNINGS - Message() << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl; + if( addedLemmas>10000 ){ + Debug("fmf-exit") << std::endl; + debugPrint("fmf-exit"); + exit( 0 ); + } #endif - }else{ - Debug("inst-fmf-ei") << " Model literal definitions:" << std::endl; - for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){ - Debug("inst-fmf-ei") << " " << d_builder.d_quant_selection_lits[f][i] << std::endl; + if( optOneQuantPerRound() && addedLemmas>0 ){ + break; } } - RepSetIterator riter( f, d_quantEngine->getModel() ); - //set the domain for the iterator (the sufficient set of instantiations to try) - if( useRelInstDomain ){ - riter.setDomain( d_rel_domain.d_quant_inst_domain[f] ); + Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; + Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; +} + +int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ + int addedLemmas = 0; + //keep track of total instantiations for statistics + int totalInst = 1; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + TypeNode tn = f[0][i].getType(); + if( d_quantEngine->getModel()->d_rep_set.hasType( tn ) ){ + totalInst = totalInst * (int)d_quantEngine->getModel()->d_rep_set.d_type_reps[ tn ].size(); + } } - RepSetEvaluator reval( d_quantEngine->getModel(), &riter ); - while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){ - d_testLemmas++; - if( d_builder.optUseModel() ){ - //see if instantiation is already true in current model - Debug("fmf-model-eval") << "Evaluating "; - riter.debugPrintSmall("fmf-model-eval"); - Debug("fmf-model-eval") << "Done calculating terms." << std::endl; - tests++; - //if evaluate(...)==1, then the instantiation is already true in the model - // depIndex is the index of the least significant variable that this evaluation relies upon - int depIndex = riter.getNumTerms()-1; - int eval = reval.evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), depIndex ); + d_totalLemmas += totalInst; + //if we need to consider this quantifier on this iteration + if( d_builder.isQuantifierActive( f ) ){ + Trace("rel-dom") << "Exhaustive instantiate " << f << std::endl; + if( useRelInstDomain ){ + Trace("rel-dom") << "Relevant domain : " << std::endl; + for( size_t i=0; i<d_rel_domain.d_quant_inst_domain[f].size(); i++ ){ + Trace("rel-dom") << " " << i << " : "; + for( size_t j=0; j<d_rel_domain.d_quant_inst_domain[f][i].size(); j++ ){ + Trace("rel-dom") << d_rel_domain.d_quant_inst_domain[f][i][j] << " "; + } + Trace("rel-dom") << std::endl; + } + } + int tests = 0; + int triedLemmas = 0; + Debug("inst-fmf-ei") << "Add matches for " << f << "..." << std::endl; + Debug("inst-fmf-ei") << " Instantiation Constants: "; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; + } + Debug("inst-fmf-ei") << std::endl; + RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) ); + riter.setQuantifier( f ); + //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round + d_incomplete_check = d_incomplete_check || riter.d_incomplete; + //set the domain for the iterator (the sufficient set of instantiations to try) + if( useRelInstDomain ){ + riter.setDomain( d_rel_domain.d_quant_inst_domain[f] ); + } + d_quantEngine->getModel()->resetEvaluate(); + while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){ + d_testLemmas++; + int eval = 0; + int depIndex; + if( d_builder.optUseModel() ){ + //see if instantiation is already true in current model + Debug("fmf-model-eval") << "Evaluating "; + riter.debugPrintSmall("fmf-model-eval"); + Debug("fmf-model-eval") << "Done calculating terms." << std::endl; + tests++; + //if evaluate(...)==1, then the instantiation is already true in the model + // depIndex is the index of the least significant variable that this evaluation relies upon + depIndex = riter.getNumTerms()-1; + eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), depIndex, &riter ); + if( eval==1 ){ + Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; + }else{ + Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl; + } + } if( eval==1 ){ - Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; + //instantiation is already true -> skip riter.increment2( depIndex ); }else{ - Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl; + //instantiation was not shown to be true, construct the match InstMatch m; - riter.getMatch( d_quantEngine, m ); + for( int i=0; i<riter.getNumTerms(); i++ ){ + m.set( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, riter.d_index_order[i] ), riter.getTerm( i ) ); + } Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; triedLemmas++; d_triedLemmas++; + //add as instantiation if( d_quantEngine->addInstantiation( f, m ) ){ addedLemmas++; #ifdef EVAL_FAIL_SKIP_MULTIPLE @@ -270,70 +338,48 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ riter.increment(); } } - }else{ - InstMatch m; - riter.getMatch( d_quantEngine, m ); - Debug("fmf-model-eval") << "* Add instantiation " << std::endl; - triedLemmas++; - d_triedLemmas++; - if( d_quantEngine->addInstantiation( f, m ) ){ - addedLemmas++; - } - riter.increment(); } - } - d_statistics.d_eval_formulas += reval.d_eval_formulas; - d_statistics.d_eval_uf_terms += reval.d_eval_uf_terms; - d_statistics.d_eval_lits += reval.d_eval_lits; - d_statistics.d_eval_lits_unknown += reval.d_eval_lits_unknown; - int totalInst = 1; - int relevantInst = 1; - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - totalInst = totalInst * (int)d_quantEngine->getModel()->d_rep_set.d_type_reps[ f[0][i].getType() ].size(); - relevantInst = relevantInst * (int)riter.d_domain[i].size(); - } - d_totalLemmas += totalInst; - d_relevantLemmas += relevantInst; - Debug("inst-fmf-ei") << "Finished: " << std::endl; - Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl; - Debug("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl; - Debug("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl; - Debug("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; - Debug("inst-fmf-ei") << " # Tests: " << tests << std::endl; -///----------- + d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas; + d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms; + d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits; + d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown; + int relevantInst = 1; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + relevantInst = relevantInst * (int)riter.d_domain[i].size(); + } + d_relevantLemmas += relevantInst; + Debug("inst-fmf-ei") << "Finished: " << std::endl; + Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl; + Debug("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl; + Debug("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl; + Debug("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; + Debug("inst-fmf-ei") << " # Tests: " << tests << std::endl; #ifdef ME_PRINT_WARNINGS - if( addedLemmas>1000 ){ - Notice() << "WARNING: many instantiations produced for " << f << ": " << std::endl; - Notice() << " Inst Total: " << totalInst << std::endl; - Notice() << " Inst Relevant: " << totalRelevant << std::endl; - Notice() << " Inst Tried: " << triedLemmas << std::endl; - Notice() << " Inst Added: " << addedLemmas << std::endl; - Notice() << " # Tests: " << tests << std::endl; - Notice() << std::endl; - if( !d_builder.d_quant_selection_lits[f].empty() ){ - Notice() << " Model literal definitions:" << std::endl; - for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){ - Notice() << " " << d_builder.d_quant_selection_lits[f][i] << std::endl; - } + if( addedLemmas>1000 ){ + Notice() << "WARNING: many instantiations produced for " << f << ": " << std::endl; + Notice() << " Inst Total: " << totalInst << std::endl; + Notice() << " Inst Relevant: " << totalRelevant << std::endl; + Notice() << " Inst Tried: " << triedLemmas << std::endl; + Notice() << " Inst Added: " << addedLemmas << std::endl; + Notice() << " # Tests: " << tests << std::endl; Notice() << std::endl; } - } #endif -///----------- + } return addedLemmas; } void ModelEngine::debugPrint( const char* c ){ - Debug( c ) << "Quantifiers: " << std::endl; + Trace( c ) << "Quantifiers: " << std::endl; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); - Debug( c ) << " "; - if( d_builder.d_quant_sat.find( f )!=d_builder.d_quant_sat.end() ){ - Debug( c ) << "*SAT* "; + Trace( c ) << " "; + if( !d_builder.isQuantifierActive( f ) ){ + Trace( c ) << "*Inactive* "; }else{ - Debug( c ) << " "; + Trace( c ) << " "; } - Debug( c ) << f << std::endl; + Trace( c ) << f << std::endl; } //d_quantEngine->getModel()->debugPrint( c ); } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index f5d1db736..a292eb5f8 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -40,6 +40,8 @@ private: //data maintained globally: private: //analysis of current model: //relevant domain RelevantDomain d_rel_domain; + //is the exhaustive instantiation incomplete? + bool d_incomplete_check; private: //options bool optOneInstPerQuantRound(); @@ -48,6 +50,8 @@ private: private: //initialize quantifiers, return number of lemmas produced int initializeQuantifier( Node f ); + //check model + void checkModel( int& addedLemmas ); //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced int exhaustiveInstantiate( Node f, bool useRelInstDomain = false ); private: @@ -57,7 +61,7 @@ private: int d_totalLemmas; int d_relevantLemmas; public: - ModelEngine( QuantifiersEngine* qe ); + ModelEngine( context::Context* c, QuantifiersEngine* qe ); ~ModelEngine(){} public: void check( Theory::Effort e ); diff --git a/src/theory/quantifiers/inst_when_mode.cpp b/src/theory/quantifiers/modes.cpp index b60148c21..b6786d9f0 100644 --- a/src/theory/quantifiers/inst_when_mode.cpp +++ b/src/theory/quantifiers/modes.cpp @@ -2,7 +2,7 @@ /*! \file inst_when_mode.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: ajreynol ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) @@ -18,7 +18,7 @@ **/ #include <iostream> -#include "theory/quantifiers/inst_when_mode.h" +#include "theory/quantifiers/modes.h" namespace CVC4 { @@ -43,5 +43,41 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mo return out; } +std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) { + switch(mode) { + case theory::quantifiers::LITERAL_MATCH_NONE: + out << "LITERAL_MATCH_NONE"; + break; + case theory::quantifiers::LITERAL_MATCH_PREDICATE: + out << "LITERAL_MATCH_PREDICATE"; + break; + case theory::quantifiers::LITERAL_MATCH_EQUALITY: + out << "LITERAL_MATCH_EQUALITY"; + break; + default: + out << "LiteralMatchMode!UNKNOWN"; + } + + return out; +} + +std::ostream& operator<<(std::ostream& out, theory::quantifiers::AxiomInstMode mode) { + switch(mode) { + case theory::quantifiers::AXIOM_INST_MODE_DEFAULT: + out << "AXIOM_INST_MODE_DEFAULT"; + break; + case theory::quantifiers::AXIOM_INST_MODE_TRUST: + out << "AXIOM_INST_MODE_TRUST"; + break; + case theory::quantifiers::AXIOM_INST_MODE_PRIORITY: + out << "AXIOM_INST_MODE_PRIORITY"; + break; + default: + out << "AxiomInstMode!UNKNOWN"; + } + + return out; +} + }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_when_mode.h b/src/theory/quantifiers/modes.h index 2cfba4935..8c56b8f3f 100644 --- a/src/theory/quantifiers/inst_when_mode.h +++ b/src/theory/quantifiers/modes.h @@ -1,8 +1,8 @@ /********************* */ -/*! \file inst_when_mode.h +/*! \file modes.h ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: ajreynol ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) @@ -19,8 +19,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H -#define __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H +#ifndef __CVC4__THEORY__QUANTIFIERS__MODEs_H +#define __CVC4__THEORY__QUANTIFIERS__MODEs_H #include <iostream> @@ -39,6 +39,25 @@ typedef enum { INST_WHEN_LAST_CALL, } InstWhenMode; +typedef enum { + /** Do not consider polarity of patterns */ + LITERAL_MATCH_NONE, + /** Consider polarity of boolean predicates only */ + LITERAL_MATCH_PREDICATE, + /** Consider polarity of boolean predicates, as well as equalities */ + LITERAL_MATCH_EQUALITY, +} LiteralMatchMode; + +typedef enum { + /** default, use all methods for axioms */ + AXIOM_INST_MODE_DEFAULT, + /** only use heuristic methods for axioms, return unknown in the case no instantiations are produced */ + AXIOM_INST_MODE_TRUST, + /** only use heuristic methods for axioms, resort to all methods when no instantiations are produced */ + AXIOM_INST_MODE_PRIORITY, +} AxiomInstMode; + + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 91e831092..a28ccb423 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -45,13 +45,13 @@ option smartTriggers /--disable-smart-triggers bool :default true option registerQuantBodyTerms --register-quant-body-terms bool :default false consider ground terms within bodies of quantified formulas for matching -option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :include "theory/quantifiers/inst_when_mode.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" +option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" when to apply instantiation - + option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly -option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/literal_match_mode.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" +option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" choose literal matching mode option cbqi --enable-cbqi/--disable-cbqi bool :default false @@ -67,23 +67,23 @@ option flipDecision --enable-flip-decision/ bool :default false option finiteModelFind --finite-model-find bool :default false use finite model finding heuristic for quantifier instantiation -option ufssRegions /--disable-uf-ss-regions bool :default true - disable region-based method for discovering cliques and splits in uf strong solver -option ufssEagerSplits --uf-ss-eager-split bool :default false - add splits eagerly for uf strong solver -option ufssColoringSat --uf-ss-coloring-sat bool :default false - use coloring-based SAT heuristic for uf strong solver - option fmfModelBasedInst /--disable-fmf-mbqi bool :default true disable model-based quantifier instantiation for finite model finding -option fmfInstGen /--disable-fmf-inst-gen bool :default true - disable Inst-Gen instantiation techniques for finite model finding option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false only add one instantiation per quantifier per round for fmf +option fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false + only add instantiations for one quantifier per round for fmf option fmfInstEngine --fmf-inst-engine bool :default false use instantiation engine in conjunction with finite model finding option fmfRelevantDomain --fmf-relevant-domain bool :default false use relevant domain computation, similar to complete instantiation (Ge, deMoura 09) +option fmfInstGen /--disable-fmf-inst-gen bool :default true + disable Inst-Gen instantiation techniques for finite model finding +option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false + only perform Inst-Gen instantiation techniques on one quantifier per round + +option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" + policy for instantiating axioms endmodule diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 24734e8c8..00e91d115 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -58,6 +58,23 @@ predicate\n\ \n\ "; +static const std::string axiomInstModeHelp = "\ +Literal match modes currently supported by the --axiom-inst option:\n\ +\n\ +default \n\ ++ Treat axioms the same as usual quantifiers, i.e. use all available methods for\n\ + instantiating axioms.\n\ +\n\ +trust \n\ ++ Treat axioms only using heuristic instantiation. Return unknown if in the case\n\ + that no instantiations are produced.\n\ +\n\ +priority \n\ ++ Treat axioms only using heuristic instantiation. Resort to using all methods\n\ + in the case that no instantiations are produced.\n\ +\n\ +"; + inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { return INST_WHEN_PRE_FULL; @@ -104,6 +121,22 @@ inline void checkLiteralMatchMode(std::string option, LiteralMatchMode mode, Smt } } +inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "default") { + return AXIOM_INST_MODE_DEFAULT; + } else if(optarg == "trust") { + return AXIOM_INST_MODE_TRUST; + } else if(optarg == "priority") { + return AXIOM_INST_MODE_PRIORITY; + } else if(optarg == "help") { + puts(axiomInstModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --axiom-inst: `") + + optarg + "'. Try --axiom-inst help."); + } +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp new file mode 100644 index 000000000..22ee66362 --- /dev/null +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -0,0 +1,43 @@ +/********************* */
+/*! \file quantifiers_attributes.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of QuantifiersAttributes class
+ **/
+
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/options.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+void QuantifiersAttributes::setUserAttribute( std::string& attr, Node n ){
+ if( n.getKind()==FORALL ){
+ if( attr=="axiom" ){
+ Trace("quant-attr") << "Set axiom " << n << std::endl;
+ AxiomAttribute aa;
+ n.setAttribute( aa, true );
+ }else if( attr=="conjecture" ){
+ Trace("quant-attr") << "Set conjecture " << n << std::endl;
+ ConjectureAttribute ca;
+ n.setAttribute( ca, true );
+ }
+ }else{
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ setUserAttribute( attr, n[i] );
+ }
+ }
+}
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h new file mode 100644 index 000000000..49c374f3e --- /dev/null +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -0,0 +1,53 @@ +/********************* */
+/*! \file quantifiers_attributes.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Attributes for the theory quantifiers
+ **
+ ** Attributes for the theory quantifiers.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
+#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
+
+#include "theory/rewriter.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Attribute true for quantifiers that are axioms */
+struct AxiomAttributeId {};
+typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
+
+/** Attribute true for quantifiers that are conjecture */
+struct ConjectureAttributeId {};
+typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
+
+struct QuantifiersAttributes
+{
+ /** set user attribute
+ * This function will apply a custom set of attributes to all top-level universal
+ * quantifiers contained in n
+ */
+ static void setUserAttribute( std::string& attr, Node n );
+};
+
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 1563a3d1d..495e0f7a4 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -26,16 +26,18 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -RelevantDomain::RelevantDomain( FirstOrderModel* m ) : d_model( m ){ +RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){ } void RelevantDomain::compute(){ + Trace("rel-dom") << "compute relevant domain" << std::endl; d_quant_inst_domain.clear(); for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ Node f = d_model->getAssertedQuantifier( i ); d_quant_inst_domain[f].resize( f[0].getNumChildren() ); } + Trace("rel-dom") << "account for ground terms" << std::endl; //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment) for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin(); it != d_model->d_uf_model_tree.end(); ++it ){ @@ -47,6 +49,7 @@ void RelevantDomain::compute(){ if( d_model->d_rep_set.hasType( n[j].getType() ) ){ Node ra = d_model->getRepresentative( n[j] ); int raIndex = d_model->d_rep_set.getIndexFor( ra ); + if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground domain: rep set does not contain : " << ra << std::endl; Assert( raIndex!=-1 ); if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){ d_active_domain[op][j].push_back( raIndex ); @@ -56,12 +59,14 @@ void RelevantDomain::compute(){ //add to range Node r = d_model->getRepresentative( n ); int raIndex = d_model->d_rep_set.getIndexFor( r ); + if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground range: rep set does not contain : " << r << std::endl; Assert( raIndex!=-1 ); if( std::find( d_active_range[op].begin(), d_active_range[op].end(), raIndex )==d_active_range[op].end() ){ d_active_range[op].push_back( raIndex ); } } } + Trace("rel-dom") << "do quantifiers" << std::endl; //find fixed point for relevant domain computation bool success; do{ @@ -69,19 +74,20 @@ void RelevantDomain::compute(){ for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ Node f = d_model->getAssertedQuantifier( i ); //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment) - if( computeRelevantInstantiationDomain( d_model->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, d_quant_inst_domain[f] ) ){ + if( computeRelevantInstantiationDomain( d_qe->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, f ) ){ success = false; } //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment) RepDomain range; - if( extendFunctionDomains( d_model->getTermDatabase()->getCounterexampleBody( f ), range ) ){ + if( extendFunctionDomains( d_qe->getTermDatabase()->getCounterexampleBody( f ), range ) ){ success = false; } } }while( !success ); + Trace("rel-dom") << "done compute relevant domain" << std::endl; } -bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ){ +bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f ){ bool domainChanged = false; if( n.getKind()==INST_CONSTANT ){ bool domainSet = false; @@ -93,8 +99,9 @@ bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, in if( d_active_domain.find( op )!=d_active_domain.end() ){ for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){ int d = d_active_domain[op][arg][i]; - if( std::find( rd[vi].begin(), rd[vi].end(), d )==rd[vi].end() ){ - rd[vi].push_back( d ); + if( std::find( d_quant_inst_domain[f][vi].begin(), d_quant_inst_domain[f][vi].end(), d )== + d_quant_inst_domain[f][vi].end() ){ + d_quant_inst_domain[f][vi].push_back( d ); domainChanged = true; } } @@ -104,21 +111,21 @@ bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, in if( !domainSet ){ //otherwise, we must consider the entire domain TypeNode tn = n.getType(); - if( d_model->d_rep_set.hasType( tn ) ){ - if( rd[vi].size()!=d_model->d_rep_set.d_type_reps[tn].size() ){ - rd[vi].clear(); + if( d_quant_inst_domain_complete[f].find( vi )==d_quant_inst_domain_complete[f].end() ){ + if( d_model->d_rep_set.hasType( tn ) ){ + //it is the complete domain + d_quant_inst_domain[f][vi].clear(); for( size_t i=0; i<d_model->d_rep_set.d_type_reps[tn].size(); i++ ){ - rd[vi].push_back( i ); - domainChanged = true; + d_quant_inst_domain[f][vi].push_back( i ); } + domainChanged = true; } - }else{ - //infinite domain? + d_quant_inst_domain_complete[f][vi] = true; } } }else{ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( computeRelevantInstantiationDomain( n[i], n, i, rd ) ){ + if( computeRelevantInstantiationDomain( n[i], n, i, f ) ){ domainChanged = true; } } @@ -166,7 +173,13 @@ bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){ } }else{ Node r = d_model->getRepresentative( n ); - range.push_back( d_model->d_rep_set.getIndexFor( r ) ); + int index = d_model->d_rep_set.getIndexFor( r ); + if( index==-1 ){ + //we consider all ground terms in bodies of quantifiers to be the first ground representative + range.push_back( 0 ); + }else{ + range.push_back( index ); + } } return domainChanged; } diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 6ce47d114..62522812a 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -28,6 +28,7 @@ namespace quantifiers { class RelevantDomain { private: + QuantifiersEngine* d_qe; FirstOrderModel* d_model; //the domain of the arguments for each operator @@ -35,16 +36,17 @@ private: //the range for each operator std::map< Node, RepDomain > d_active_range; //for computing relevant instantiation domain, return true if changed - bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ); + bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f ); //for computing extended bool extendFunctionDomains( Node n, RepDomain& range ); public: - RelevantDomain( FirstOrderModel* m ); + RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ); virtual ~RelevantDomain(){} //compute the relevant domain void compute(); //relevant instantiation domain for each quantifier std::map< Node, std::vector< RepDomain > > d_quant_inst_domain; + std::map< Node, std::map< int, bool > > d_quant_inst_domain_complete; };/* class RelevantDomain */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp deleted file mode 100644 index 7461f3477..000000000 --- a/src/theory/quantifiers/rep_set_iterator.cpp +++ /dev/null @@ -1,517 +0,0 @@ -/********************* */ -/*! \file rep_set_iterator.cpp - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of relevant domain class - **/ - -#include "theory/quantifiers/rep_set_iterator.h" -#include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/term_database.h" - -#define USE_INDEX_ORDERING - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - -RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_model( model ){ - //store instantiation constants - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - d_index.push_back( 0 ); - } - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - //store default index order - d_index_order.push_back( i ); - d_var_order[i] = i; - //store default domain - d_domain.push_back( RepDomain() ); - TypeNode tn = d_f[0][i].getType(); - if( tn.isSort() ){ - if( d_model->d_rep_set.hasType( tn ) ){ - for( int j=0; j<(int)d_model->d_rep_set.d_type_reps[d_f[0][i].getType()].size(); j++ ){ - d_domain[i].push_back( j ); - } - }else{ - Unimplemented("Cannot create instantiation iterator for unknown uninterpretted sort"); - } - }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ - Unimplemented("Cannot create instantiation iterator for arithmetic quantifier"); - }else if( tn.isDatatype() ){ - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - //if finite, then use type enumerator - if( dt.isFinite() ){ - //DO_THIS: use type enumerator - Unimplemented("Not yet implemented: instantiation iterator for finite datatype quantifier"); - }else{ - Unimplemented("Cannot create instantiation iterator for infinite datatype quantifier"); - } - }else{ - Unimplemented("Cannot create instantiation iterator for quantifier"); - } - } -} - -void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){ - d_index_order.clear(); - d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() ); - //make the d_var_order mapping - for( int i=0; i<(int)d_index_order.size(); i++ ){ - d_var_order[d_index_order[i]] = i; - } -} - -void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){ - d_domain.clear(); - d_domain.insert( d_domain.begin(), domain.begin(), domain.end() ); - //we are done if a domain is empty - for( int i=0; i<(int)d_domain.size(); i++ ){ - if( d_domain[i].empty() ){ - d_index.clear(); - } - } -} - -void RepSetIterator::increment2( int counter ){ - Assert( !isFinished() ); -#ifdef DISABLE_EVAL_SKIP_MULTIPLE - counter = (int)d_index.size()-1; -#endif - //increment d_index - while( counter>=0 && d_index[counter]==(int)(d_domain[counter].size()-1) ){ - counter--; - } - if( counter==-1 ){ - d_index.clear(); - }else{ - for( int i=(int)d_index.size()-1; i>counter; i-- ){ - d_index[i] = 0; - //d_model->clearEvalFailed( i ); - } - d_index[counter]++; - //d_model->clearEvalFailed( counter ); - } -} - -void RepSetIterator::increment(){ - if( !isFinished() ){ - increment2( (int)d_index.size()-1 ); - } -} - -bool RepSetIterator::isFinished(){ - return d_index.empty(); -} - -void RepSetIterator::getMatch( QuantifiersEngine* qe, InstMatch& m ){ - for( int i=0; i<(int)d_index.size(); i++ ){ - m.set( qe->getTermDatabase()->getInstantiationConstant( d_f, d_index_order[i] ), getTerm( i )); - } -} - -Node RepSetIterator::getTerm( int i ){ - TypeNode tn = d_f[0][d_index_order[i]].getType(); - Assert( d_model->d_rep_set.d_type_reps.find( tn )!=d_model->d_rep_set.d_type_reps.end() ); - int index = d_index_order[i]; - return d_model->d_rep_set.d_type_reps[tn][d_domain[index][d_index[index]]]; -} - -void RepSetIterator::debugPrint( const char* c ){ - for( int i=0; i<(int)d_index.size(); i++ ){ - Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl; - } -} - -void RepSetIterator::debugPrintSmall( const char* c ){ - Debug( c ) << "RI: "; - for( int i=0; i<(int)d_index.size(); i++ ){ - Debug( c ) << d_index[i] << ": " << getTerm( i ) << " "; - } - Debug( c ) << std::endl; -} - -RepSetEvaluator::RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ) : d_model( m ), d_riter( ri ){ - d_eval_formulas = 0; - d_eval_uf_terms = 0; - d_eval_lits = 0; - d_eval_lits_unknown = 0; -} - -//if evaluate( n ) = eVal, -// let n' = d_riter * n be the formula n instantiated with the current values in r_iter -// if eVal = 1, then n' is true, if eVal = -1, then n' is false, -// if eVal = 0, then n' cannot be proven to be equal to phaseReq -// if eVal is not 0, then -// each n{d_riter->d_index[0]/x_0...d_riter->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model -int RepSetEvaluator::evaluate( Node n, int& depIndex ){ - ++d_eval_formulas; - //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl; - //Notice() << "Eval " << n << std::endl; - if( n.getKind()==NOT ){ - int val = evaluate( n[0], depIndex ); - return val==1 ? -1 : ( val==-1 ? 1 : 0 ); - }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){ - int baseVal = n.getKind()==AND ? 1 : -1; - int eVal = baseVal; - int posDepIndex = d_riter->getNumTerms(); - int negDepIndex = -1; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - //evaluate subterm - int childDepIndex; - Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i]; - int eValT = evaluate( nn, childDepIndex ); - if( eValT==baseVal ){ - if( eVal==baseVal ){ - if( childDepIndex>negDepIndex ){ - negDepIndex = childDepIndex; - } - } - }else if( eValT==-baseVal ){ - eVal = -baseVal; - if( childDepIndex<posDepIndex ){ - posDepIndex = childDepIndex; - if( posDepIndex==-1 ){ - break; - } - } - }else if( eValT==0 ){ - if( eVal==baseVal ){ - eVal = 0; - } - } - } - if( eVal!=0 ){ - depIndex = eVal==-baseVal ? posDepIndex : negDepIndex; - return eVal; - }else{ - return 0; - } - }else if( n.getKind()==IFF || n.getKind()==XOR ){ - int depIndex1; - int eVal = evaluate( n[0], depIndex1 ); - if( eVal!=0 ){ - int depIndex2; - int eVal2 = evaluate( n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2 ); - if( eVal2!=0 ){ - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - return eVal==eVal2 ? 1 : -1; - } - } - return 0; - }else if( n.getKind()==ITE ){ - int depIndex1, depIndex2; - int eVal = evaluate( n[0], depIndex1 ); - if( eVal==0 ){ - //evaluate children to see if they are the same value - int eval1 = evaluate( n[1], depIndex1 ); - if( eval1!=0 ){ - int eval2 = evaluate( n[1], depIndex2 ); - if( eval1==eval2 ){ - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - return eval1; - } - } - }else{ - int eValT = evaluate( n[eVal==1 ? 1 : 2], depIndex2 ); - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - return eValT; - } - return 0; - }else if( n.getKind()==FORALL ){ - return 0; - }else{ - ++d_eval_lits; - ////if we know we will fail again, immediately return - //if( d_eval_failed.find( n )!=d_eval_failed.end() ){ - // if( d_eval_failed[n] ){ - // return -1; - // } - //} - //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl; - int retVal = 0; - depIndex = d_riter->getNumTerms()-1; - Node val = evaluateTerm( n, depIndex ); - if( !val.isNull() ){ - if( d_model->areEqual( val, d_model->d_true ) ){ - retVal = 1; - }else if( d_model->areEqual( val, d_model->d_false ) ){ - retVal = -1; - }else{ - if( val.getKind()==EQUAL ){ - if( d_model->areEqual( val[0], val[1] ) ){ - retVal = 1; - }else if( d_model->areDisequal( val[0], val[1] ) ){ - retVal = -1; - } - } - } - } - if( retVal!=0 ){ - Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl; - }else{ - ++d_eval_lits_unknown; - Debug("fmf-eval-amb") << "Neither true nor false : " << n << std::endl; - //std::cout << "Neither true nor false : " << n << std::endl; - //std::cout << " Value : " << val << std::endl; - //for( int i=0; i<(int)n.getNumChildren(); i++ ){ - // std::cout << " " << i << " : " << n[i].getType() << std::endl; - //} - } - return retVal; - } -} - -Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){ - //Message() << "Eval term " << n << std::endl; - if( !n.hasAttribute(InstConstantAttribute()) ){ - //if evaluating a ground term, just consult the standard getValue functionality - depIndex = -1; - return d_model->getValue( n ); - }else{ - Node val; - depIndex = d_riter->getNumTerms()-1; - //check the type of n - if( n.getKind()==INST_CONSTANT ){ - int v = n.getAttribute(InstVarNumAttribute()); - depIndex = d_riter->d_var_order[ v ]; - val = d_riter->getTerm( v ); - }else if( n.getKind()==ITE ){ - int depIndex1, depIndex2; - int eval = evaluate( n[0], depIndex1 ); - if( eval==0 ){ - //evaluate children to see if they are the same - Node val1 = evaluateTerm( n[ 1 ], depIndex1 ); - Node val2 = evaluateTerm( n[ 2 ], depIndex2 ); - if( val1==val2 ){ - val = val1; - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - }else{ - return Node::null(); - } - }else{ - val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2 ); - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - } - }else{ - std::vector< int > children_depIndex; - //for select, pre-process read over writes - if( n.getKind()==SELECT ){ -#if 1 - //std::cout << "Evaluate " << n << std::endl; - Node sel = evaluateTerm( n[1], depIndex ); - if( sel.isNull() ){ - depIndex = d_riter->getNumTerms()-1; - return Node::null(); - } - Node arr = d_model->getRepresentative( n[0] ); - //if( n[0]!=d_model->getRepresentative( n[0] ) ){ - // std::cout << n[0] << " is " << d_model->getRepresentative( n[0] ) << std::endl; - //} - int tempIndex; - int eval = 1; - while( arr.getKind()==STORE && eval!=0 ){ - eval = evaluate( sel.eqNode( arr[1] ), tempIndex ); - depIndex = tempIndex > depIndex ? tempIndex : depIndex; - if( eval==1 ){ - val = evaluateTerm( arr[2], tempIndex ); - depIndex = tempIndex > depIndex ? tempIndex : depIndex; - return val; - }else if( eval==-1 ){ - arr = arr[0]; - } - } - arr = evaluateTerm( arr, tempIndex ); - depIndex = tempIndex > depIndex ? tempIndex : depIndex; - val = NodeManager::currentNM()->mkNode( SELECT, arr, sel ); -#else - val = evaluateTermDefault( n, depIndex, children_depIndex ); -#endif - }else{ - //default term evaluate : evaluate all children, recreate the value - val = evaluateTermDefault( n, depIndex, children_depIndex ); - } - if( !val.isNull() ){ - bool setVal = false; - //custom ways of evaluating terms - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; - //if it is a defined UF, then consult the interpretation - if( d_model->d_uf_model_tree.find( op )!=d_model->d_uf_model_tree.end() ){ - ++d_eval_uf_terms; - int argDepIndex = 0; - //make the term model specifically for n - makeEvalUfModel( n ); - //now, consult the model - if( d_eval_uf_use_default[n] ){ - val = d_model->d_uf_model_tree[op].getValue( d_model, val, argDepIndex ); - }else{ - val = d_eval_uf_model[ n ].getValue( d_model, val, argDepIndex ); - } - //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; - //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe ); - Assert( !val.isNull() ); - //recalculate the depIndex - depIndex = -1; - for( int i=0; i<argDepIndex; i++ ){ - int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i]; - Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl; - if( children_depIndex[index]>depIndex ){ - depIndex = children_depIndex[index]; - } - } - setVal = true; - } - }else if( n.getKind()==SELECT ){ - //we are free to interpret this term however we want - } - //if not set already, rewrite and consult model for interpretation - if( !setVal ){ - val = Rewriter::rewrite( val ); - if( !val.isConst() ){ - //FIXME: we cannot do this until we trust all theories collectModelInfo! - //val = d_model->getInterpretedValue( val ); - //val = d_model->getRepresentative( val ); - } - } - Debug("fmf-eval-debug") << "Evaluate term " << n << " = "; - d_model->printRepresentativeDebug( "fmf-eval-debug", val ); - Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl; - } - } - return val; - } -} - -Node RepSetEvaluator::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ){ - depIndex = -1; - if( n.getNumChildren()==0 ){ - return n; - }else{ - //first we must evaluate the arguments - std::vector< Node > children; - if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - //for each argument, calculate its value, and the variables its value depends upon - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - childDepIndex.push_back( -1 ); - Node nn = evaluateTerm( n[i], childDepIndex[i] ); - if( nn.isNull() ){ - depIndex = d_riter->getNumTerms()-1; - return nn; - }else{ - children.push_back( nn ); - if( childDepIndex[i]>depIndex ){ - depIndex = childDepIndex[i]; - } - } - } - //recreate the value - Node val = NodeManager::currentNM()->mkNode( n.getKind(), children ); - return val; - } -} - -void RepSetEvaluator::clearEvalFailed( int index ){ - for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){ - d_eval_failed[ d_eval_failed_lits[index][i] ] = false; - } - d_eval_failed_lits[index].clear(); -} - -void RepSetEvaluator::makeEvalUfModel( Node n ){ - if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){ - makeEvalUfIndexOrder( n ); - if( !d_eval_uf_use_default[n] ){ - Node op = n.getOperator(); - d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] ); - d_model->d_uf_model_gen[op].makeModel( d_model, d_eval_uf_model[n] ); - //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl; - //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 ); - } - } -} - -struct sortGetMaxVariableNum { - std::map< Node, int > d_max_var_num; - int computeMaxVariableNum( Node n ){ - if( n.getKind()==INST_CONSTANT ){ - return n.getAttribute(InstVarNumAttribute()); - }else if( n.hasAttribute(InstConstantAttribute()) ){ - int maxVal = -1; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - int val = getMaxVariableNum( n[i] ); - if( val>maxVal ){ - maxVal = val; - } - } - return maxVal; - }else{ - return -1; - } - } - int getMaxVariableNum( Node n ){ - std::map< Node, int >::iterator it = d_max_var_num.find( n ); - if( it==d_max_var_num.end() ){ - int num = computeMaxVariableNum( n ); - d_max_var_num[n] = num; - return num; - }else{ - return it->second; - } - } - bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));} -}; - -void RepSetEvaluator::makeEvalUfIndexOrder( Node n ){ - if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){ -#ifdef USE_INDEX_ORDERING - //sort arguments in order of least significant vs. most significant variable in default ordering - std::map< Node, std::vector< int > > argIndex; - std::vector< Node > args; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( argIndex.find( n[i] )==argIndex.end() ){ - args.push_back( n[i] ); - } - argIndex[n[i]].push_back( i ); - } - sortGetMaxVariableNum sgmvn; - std::sort( args.begin(), args.end(), sgmvn ); - for( int i=0; i<(int)args.size(); i++ ){ - for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){ - d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] ); - } - } - bool useDefault = true; - for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ - if( i!=d_eval_term_index_order[n][i] ){ - useDefault = false; - break; - } - } - d_eval_uf_use_default[n] = useDefault; - Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : "; - for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ - Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " "; - } - Debug("fmf-index-order") << std::endl; -#else - d_eval_uf_use_default[n] = true; -#endif - } -} - - diff --git a/src/theory/quantifiers/rep_set_iterator.h b/src/theory/quantifiers/rep_set_iterator.h deleted file mode 100644 index 85a2f3fd2..000000000 --- a/src/theory/quantifiers/rep_set_iterator.h +++ /dev/null @@ -1,119 +0,0 @@ -/********************* */ -/*! \file rep_set_iterator.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief rep_set_iterator class - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__QUANTIFIERS__REP_SET_ITERATOR_H -#define __CVC4__THEORY__QUANTIFIERS__REP_SET_ITERATOR_H - -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/first_order_model.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -/** this class iterates over a RepSet */ -class RepSetIterator { -public: - RepSetIterator( Node f, FirstOrderModel* model ); - ~RepSetIterator(){} - //pointer to quantifier - Node d_f; - //pointer to model - FirstOrderModel* d_model; - //index we are considering - std::vector< int > d_index; - //domain we are considering - std::vector< RepDomain > d_domain; - //ordering for variables we are indexing over - // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 }, - // then we consider instantiations in this order: - // a/x a/y a/z - // a/x b/y a/z - // b/x a/y a/z - // b/x b/y a/z - // ... - std::vector< int > d_index_order; - //variables to index they are considered at - // for example, if d_index_order = { 2, 0, 1 } - // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 } - std::map< int, int > d_var_order; - //the instantiation constants of d_f - std::vector< Node > d_ic; - //the current terms we are considering - std::vector< Node > d_terms; -public: - /** set index order */ - void setIndexOrder( std::vector< int >& indexOrder ); - /** set domain */ - void setDomain( std::vector< RepDomain >& domain ); - /** increment the iterator */ - void increment2( int counter ); - void increment(); - /** is the iterator finished? */ - bool isFinished(); - /** produce the match that this iterator represents */ - void getMatch( QuantifiersEngine* qe, InstMatch& m ); - /** get the i_th term we are considering */ - Node getTerm( int i ); - /** get the number of terms we are considering */ - int getNumTerms() { return d_f[0].getNumChildren(); } - /** debug print */ - void debugPrint( const char* c ); - void debugPrintSmall( const char* c ); -}; - -class RepSetEvaluator -{ -private: - FirstOrderModel* d_model; - RepSetIterator* d_riter; -private: //for Theory UF: - //map from terms to the models used to calculate their value - std::map< Node, bool > d_eval_uf_use_default; - std::map< Node, uf::UfModelTree > d_eval_uf_model; - void makeEvalUfModel( Node n ); - //index ordering to use for each term - std::map< Node, std::vector< int > > d_eval_term_index_order; - int getMaxVariableNum( int n ); - void makeEvalUfIndexOrder( Node n ); -private: - //default evaluate term function - Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ); - //temporary storing which literals have failed - void clearEvalFailed( int index ); - std::map< Node, bool > d_eval_failed; - std::map< int, std::vector< Node > > d_eval_failed_lits; -public: - RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ); - virtual ~RepSetEvaluator(){} - /** evaluate functions */ - int evaluate( Node n, int& depIndex ); - Node evaluateTerm( Node n, int& depIndex ); -public: - //statistics - int d_eval_formulas; - int d_eval_uf_terms; - int d_eval_lits; - int d_eval_lits_unknown; -};/* class RepSetEvaluator */ - -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index a73d42a31..bd6b03a78 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -131,7 +131,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ if( !it->second.empty() ){ - if( it->second[0].getType()==NodeManager::currentNM()->booleanType() ){ + if( it->second[0].getType().isBoolean() ){ d_pred_map_trie[ 0 ][ it->first ].d_data.clear(); d_pred_map_trie[ 1 ][ it->first ].d_data.clear(); }else{ @@ -199,6 +199,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ ss << Expr::setlanguage(options::outputLanguage()); ss << "e_" << tn; mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn ); + Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl; }else{ mbt = d_type_map[ tn ][ 0 ]; } @@ -337,12 +338,13 @@ Node TermDb::getFreeVariableForInstConstant( Node n ){ TypeNode tn = n.getType(); if( d_free_vars.find( tn )==d_free_vars.end() ){ //if integer or real, make zero - if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ + if( tn.isInteger() || tn.isReal() ){ Rational z(0); d_free_vars[tn] = NodeManager::currentNM()->mkConst( z ); }else{ if( d_type_map[ tn ].empty() ){ d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( tn ); + Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl; }else{ d_free_vars[tn] = d_type_map[ tn ][ 0 ]; } diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 3d41d28b7..c45626dd9 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -24,11 +24,10 @@ #include "theory/quantifiers/model_engine.h" #include "expr/kind.h" #include "util/Assert.h" -#include <map> -#include <time.h> #include "theory/quantifiers/theory_quantifiers_instantiator.h" #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/quantifiers_attributes.h" using namespace std; using namespace CVC4; @@ -42,6 +41,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output d_numRestarts(0){ d_numInstantiations = 0; d_baseDecLevel = -1; + out.handleUserAttribute( "axiom", this ); + out.handleUserAttribute( "conjecture", this ); } @@ -89,7 +90,7 @@ Node TheoryQuantifiers::getValue(TNode n) { } } -void TheoryQuantifiers::collectModelInfo( TheoryModel* m ){ +void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){ } @@ -126,9 +127,12 @@ void TheoryQuantifiers::check(Effort e) { } void TheoryQuantifiers::propagate(Effort level){ - CodeTimer codeTimer(d_theoryTime); + //CodeTimer codeTimer(d_theoryTime); + //getQuantifiersEngine()->propagate( level ); +} - getQuantifiersEngine()->propagate( level ); +Node TheoryQuantifiers::getNextDecisionRequest(){ + return getQuantifiersEngine()->getNextDecisionRequest(); } void TheoryQuantifiers::assertUniversal( Node n ){ @@ -186,6 +190,6 @@ bool TheoryQuantifiers::restart(){ } } -void TheoryQuantifiers::performCheck(Effort e){ - getQuantifiersEngine()->check( e ); +void TheoryQuantifiers::setUserAttribute( std::string& attr, Node n ){ + QuantifiersAttributes::setUserAttribute( attr, n ); } diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 1e42abd22..bc712955e 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -61,17 +61,17 @@ public: void presolve(); void check(Effort e); void propagate(Effort level); + Node getNextDecisionRequest(); Node getValue(TNode n); - void collectModelInfo( TheoryModel* m ); + void collectModelInfo( TheoryModel* m, bool fullModel ); void shutdown() { } std::string identify() const { return std::string("TheoryQuantifiers"); } bool flipDecision(); + void setUserAttribute( std::string& attr, Node n ); private: void assertUniversal( Node n ); void assertExistential( Node n ); bool restart(); -public: - void performCheck(Effort e); };/* class TheoryQuantifiers */ }/* CVC4::theory::quantifiers namespace */ |