From: Andrew Reynolds Date: Tue, 11 Dec 2018 22:38:00 +0000 (-0600) Subject: Remove alternate versions of mbqi (#2742) X-Git-Tag: cvc5-1.0.0~4328 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=147fd723e6c13eb3dd44a43073be03a64ea3fe66;p=cvc5.git Remove alternate versions of mbqi (#2742) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9e93bd953..91c06ddd9 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -475,8 +475,6 @@ libcvc4_add_sources( theory/quantifiers/extended_rewrite.h theory/quantifiers/first_order_model.cpp theory/quantifiers/first_order_model.h - theory/quantifiers/fmf/ambqi_builder.cpp - theory/quantifiers/fmf/ambqi_builder.h theory/quantifiers/fmf/bounded_integers.cpp theory/quantifiers/fmf/bounded_integers.h theory/quantifiers/fmf/full_model_check.cpp diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 420396452..36144e70e 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -267,7 +267,8 @@ agg \n\ \n\ "; -const std::string OptionsHandler::s_mbqiModeHelp = "\ +const std::string OptionsHandler::s_mbqiModeHelp = + "\ Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ \n\ default \n\ @@ -277,12 +278,8 @@ default \n\ none \n\ + Disable model-based quantifier instantiation.\n\ \n\ -gen-ev \n\ -+ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ - model finding paper based on generalizing evaluations.\n\ -\n\ -abs \n\ -+ Use abstract MBQI algorithm (uses disjoint sets). \n\ +trust \n\ ++ Do not instantiate quantified formulas (incomplete technique).\n\ \n\ "; @@ -660,14 +657,11 @@ void OptionsHandler::checkLiteralMatchMode( theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode( std::string option, std::string optarg) { - if(optarg == "gen-ev") { - return theory::quantifiers::MBQI_GEN_EVAL; - } else if(optarg == "none") { + if (optarg == "none") + { return theory::quantifiers::MBQI_NONE; } else if(optarg == "default" || optarg == "fmc") { return theory::quantifiers::MBQI_FMC; - } else if(optarg == "abs") { - return theory::quantifiers::MBQI_ABS; } else if(optarg == "trust") { return theory::quantifiers::MBQI_TRUST; } else if(optarg == "help") { diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp index 1814a363d..b08f71c2e 100644 --- a/src/options/quantifiers_modes.cpp +++ b/src/options/quantifiers_modes.cpp @@ -64,18 +64,12 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMod std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) { switch(mode) { - case theory::quantifiers::MBQI_GEN_EVAL: - out << "MBQI_GEN_EVAL"; - break; case theory::quantifiers::MBQI_NONE: out << "MBQI_NONE"; break; case theory::quantifiers::MBQI_FMC: out << "MBQI_FMC"; break; - case theory::quantifiers::MBQI_ABS: - out << "MBQI_ABS"; - break; case theory::quantifiers::MBQI_TRUST: out << "MBQI_TRUST"; break; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 41378d2cd..eea043865 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -53,14 +53,10 @@ enum LiteralMatchMode { }; enum MbqiMode { - /** mbqi from CADE 24 paper */ - MBQI_GEN_EVAL, /** no mbqi */ MBQI_NONE, /** default, mbqi from Section 5.4.2 of AJR thesis */ MBQI_FMC, - /** abstract mbqi algorithm */ - MBQI_ABS, /** mbqi trust (produce no instantiations) */ MBQI_TRUST, }; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7abfd8273..ae20fa156 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1809,12 +1809,6 @@ void SmtEngine::setDefaults() { options::mbqiMode.set( quantifiers::MBQI_NONE ); } } - if( options::mbqiMode()==quantifiers::MBQI_ABS ){ - if( !d_logic.isPure(THEORY_UF) ){ - //MBQI_ABS is only supported in pure quantified UF - options::mbqiMode.set( quantifiers::MBQI_FMC ); - } - } if( options::fmfFunWellDefinedRelevant() ){ if( !options::fmfFunWellDefined.wasSetByUser() ){ options::fmfFunWellDefined.set( true ); @@ -1852,17 +1846,6 @@ void SmtEngine::setDefaults() { options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } } - if( options::mbqiMode()==quantifiers::MBQI_ABS ){ - if( !options::preSkolemQuant.wasSetByUser() ){ - options::preSkolemQuant.set( true ); - } - if( !options::preSkolemQuantNested.wasSetByUser() ){ - options::preSkolemQuantNested.set( true ); - } - if( !options::fmfOneInstPerRound.wasSetByUser() ){ - options::fmfOneInstPerRound.set( true ); - } - } } //apply counterexample guided instantiation options diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 0eec40de2..5eb65ed21 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -15,7 +15,6 @@ #include "theory/quantifiers/first_order_model.h" #include "options/base_options.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/fmf/ambqi_builder.h" #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/fmf/model_engine.h" @@ -414,473 +413,6 @@ unsigned FirstOrderModel::getModelBasisArg(Node n) return n.getAttribute(ModelBasisArgAttribute()); } -Node FirstOrderModelIG::UfModelTreeGenerator::getIntersection(TheoryModel* m, - Node n1, - Node n2, - bool& isGround) -{ - isGround = true; - std::vector children; - children.push_back(n1.getOperator()); - for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++) - { - if (n1[i] == n2[i]) - { - if (n1[i].getAttribute(ModelBasisAttribute())) - { - isGround = false; - } - children.push_back(n1[i]); - } - else if (n1[i].getAttribute(ModelBasisAttribute())) - { - children.push_back(n2[i]); - } - else if (n2[i].getAttribute(ModelBasisAttribute())) - { - children.push_back(n1[i]); - } - else if (m->areEqual(n1[i], n2[i])) - { - children.push_back(n1[i]); - } - else - { - return Node::null(); - } - } - return NodeManager::currentNM()->mkNode(APPLY_UF, children); -} - -void FirstOrderModelIG::UfModelTreeGenerator::setValue( - TheoryModel* m, Node n, Node v, bool ground, bool isReq) -{ - Assert(!n.isNull()); - Assert(!v.isNull()); - d_set_values[isReq ? 1 : 0][ground ? 1 : 0][n] = v; - if (!ground) - { - for (unsigned i = 0, defSize = d_defaults.size(); i < defSize; i++) - { - // for correctness, to allow variable order-independent function - // interpretations, we must ensure that the intersection of all default - // terms is also defined. - // for example, if we have that f( e, a ) = ..., and f( b, e ) = ..., - // then we must define f( b, a ). - bool isGround; - Node ni = getIntersection(m, n, d_defaults[i], isGround); - if (!ni.isNull()) - { - // if the intersection exists, and is not already defined - if (d_set_values[0][isGround ? 1 : 0].find(ni) - == d_set_values[0][isGround ? 1 : 0].end() - && d_set_values[1][isGround ? 1 : 0].find(ni) - == d_set_values[1][isGround ? 1 : 0].end()) - { - // use the current value - setValue(m, ni, v, isGround, false); - } - } - } - d_defaults.push_back(n); - } - if (isReq - && d_set_values[0][ground ? 1 : 0].find(n) - != d_set_values[0][ground ? 1 : 0].end()) - { - d_set_values[0][ground ? 1 : 0].erase(n); - } -} - -void FirstOrderModelIG::UfModelTreeGenerator::makeModel(TheoryModel* m, - uf::UfModelTree& tree) -{ - for (int j = 0; j < 2; j++) - { - for (int k = 0; k < 2; k++) - { - for (std::map::iterator it = d_set_values[j][k].begin(); - it != d_set_values[j][k].end(); - ++it) - { - tree.setValue(m, it->first, it->second, k == 1); - } - } - } - if (!d_default_value.isNull()) - { - tree.setDefaultValue(m, d_default_value); - } - tree.simplify(); -} - -void FirstOrderModelIG::UfModelTreeGenerator::clear() -{ - d_default_value = Node::null(); - for (int j = 0; j < 2; j++) - { - for (int k = 0; k < 2; k++) - { - d_set_values[j][k].clear(); - } - } - d_defaults.clear(); -} - -FirstOrderModelIG::FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name) : -FirstOrderModel(qe, c,name) { - -} - -void FirstOrderModelIG::processInitialize( bool ispre ){ - if( ispre ){ - //rebuild models - d_uf_model_tree.clear(); - d_uf_model_gen.clear(); - } -} - -void FirstOrderModelIG::processInitializeModelForTerm( Node n ){ - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){ - TypeNode tn = op.getType(); - tn = tn[ (int)tn.getNumChildren()-1 ]; - //only generate models for predicates and functions with uninterpreted range types - //if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){ - d_uf_model_tree[ op ] = uf::UfModelTree( op ); - d_uf_model_gen[ op ].clear(); - //} - } - } - /* - if( n.getType().isArray() ){ - while( n.getKind()==STORE ){ - n = n[0]; - } - Node nn = getRepresentative( n ); - if( d_array_model.find( nn )==d_array_model.end() ){ - d_array_model[nn] = arrays::ArrayModel( nn, this ); - } - } - */ -} - -//for evaluation of quantifier bodies - -void FirstOrderModelIG::resetEvaluate(){ - d_eval_uf_use_default.clear(); - d_eval_uf_model.clear(); - d_eval_term_index_order.clear(); -} - -//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 FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ - Debug("fmf-eval-debug2") << "Evaluate " << n << 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 ){ - 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 = 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( childDepIndexdepIndex2 ? 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{ - //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{ - Trace("fmf-eval-amb") << "Neither true nor false : " << n << std::endl; - Trace("fmf-eval-amb") << " value : " << val << std::endl; - } - return retVal; - } -} - -Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){ - //Message() << "Eval term " << n << std::endl; - Node val; - depIndex = ri->getNumTerms()-1; - //check the type of n - if( n.getKind()==INST_CONSTANT ){ - int v = n.getAttribute(InstVarNumAttribute()); - depIndex = ri->getIndexOrder( v ); - val = ri->getCurrentTerm( 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; - //default term evaluate : evaluate all children, recreate the value - val = evaluateTermDefault( n, depIndex, children_depIndex, ri ); - Trace("fmf-eval-debug") << "Evaluate term, value from " << n << " is " << val << std::endl; - 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() ){ - int argDepIndex = 0; - //make the term model specifically for n - makeEvalUfModel( n ); - //now, consult the model - if( d_eval_uf_use_default[n] ){ - Trace("fmf-eval-debug") << "get default" << std::endl; - val = d_uf_model_tree[ op ].getValue( this, val, argDepIndex ); - }else{ - Trace("fmf-eval-debug") << "get uf model" << std::endl; - 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; idepIndex ){ - depIndex = children_depIndex[index]; - } - } - setVal = true; - }else{ - Trace("fmf-eval-debug") << "No model." << std::endl; - } - } - //if not set already, rewrite and consult model for interpretation - if( !setVal ){ - val = Rewriter::rewrite( val ); - if( !val.isConst() ){ - return Node::null(); - } - } - Trace("fmf-eval-debug") << "Evaluate term " << n << " = "; - Trace("fmf-eval-debug") << getRepresentative(val); - Trace("fmf-eval-debug") << " (term " << val << "), depIndex = " << depIndex << std::endl; - } - } - return val; -} - -Node FirstOrderModelIG::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){ - depIndex = -1; - if( n.getNumChildren()==0 ){ - return n; - }else{ - bool isInterp = n.getKind()!=APPLY_UF; - //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{ - if( childDepIndex[i]>depIndex ){ - depIndex = childDepIndex[i]; - } - if( isInterp ){ - if( !nn.isConst() ) { - nn = getRepresentative( nn ); - } - } - children.push_back( nn ); - } - } - //recreate the value - Node val = NodeManager::currentNM()->mkNode( n.getKind(), children ); - return val; - } -} - -void FirstOrderModelIG::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( std::cout, d_qe->getModel(), 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( TermUtil::hasInstConstAttr(n) ){ - 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) > 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; - } -} - FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) : FirstOrderModel(qe, c, name){ @@ -989,128 +521,6 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); } -FirstOrderModelAbs::FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name) : -FirstOrderModel(qe, c, name) { - -} - -FirstOrderModelAbs::~FirstOrderModelAbs() -{ - for(std::map::iterator i = d_models.begin(); i != d_models.end(); ++i) { - delete (*i).second; - } -} - -void FirstOrderModelAbs::processInitialize( bool ispre ) { - if( !ispre ){ - Trace("ambqi-debug") << "Process initialize" << std::endl; - for( std::map::iterator it = d_models.begin(); it != d_models.end(); ++it ) { - Node op = it->first; - TypeNode tno = op.getType(); - Trace("ambqi-debug") << " Init " << op << " " << tno << std::endl; - for( unsigned i=0; i::iterator it = d_rep_id.find( r ); - if( it!=d_rep_id.end() ){ - return it->second; - }else{ - return 0; - } -} - -TNode FirstOrderModelAbs::getUsedRepresentative( TNode n ) { - if( hasTerm( n ) ){ - if( n.getType().isBoolean() ){ - return areEqual(n, d_true) ? d_true : d_false; - }else{ - return getRepresentative( n ); - } - }else{ - Trace("qint-debug") << "Get rep " << n << " " << n.getType() << std::endl; - Assert( d_rep_set.hasType( n.getType() ) && !d_rep_set.d_type_reps[n.getType()].empty() ); - return d_rep_set.d_type_reps[n.getType()][0]; - } -} - -Node FirstOrderModelAbs::getFunctionValue(Node op, const char* argPrefix ) { - if( d_models_valid[op] ){ - Trace("ambqi-debug") << "Get function value for " << op << std::endl; - TypeNode type = op.getType(); - std::vector< Node > vars; - for( size_t i=0; imkBoundVar( ss.str(), type[i] ); - vars.push_back( b ); - } - Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); - Node curr = d_models[op]->getFunctionValue( this, op, vars ); - Node fv = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); - Trace("ambqi-debug") << "Return " << fv << std::endl; - return fv; - }else{ - - } - return Node::null(); -} - -void FirstOrderModelAbs::processInitializeModelForTerm( Node n ) { - if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ - Node op = n.getKind()==APPLY_UF ? n.getOperator() : n; - if( d_models.find(op)==d_models.end()) { - Trace("abmqi-debug") << "init model for " << op << std::endl; - d_models[op] = new AbsDef; - d_models_valid[op] = false; - } - } -} - -void FirstOrderModelAbs::collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars ) { - for( unsigned i=0; i=0 && v<(int)q[0].getNumChildren() ); - eq_vars[v] = true; - } - collectEqVars( q, n[i], eq_vars ); - } -} - -void FirstOrderModelAbs::processInitializeQuantifier( Node q ) { - if( d_var_order.find( q )==d_var_order.end() ){ - std::map< int, bool > eq_vars; - for( unsigned i=0; i::iterator it = eq_vars.begin(); it != eq_vars.end(); ++it ){ - if( it->second==(r==1) ){ - d_var_index[q][it->first] = d_var_order[q].size(); - d_var_order[q].push_back( it->first ); - } - } - } - } -} - -Node FirstOrderModelAbs::getVariable( Node q, unsigned i ) { - return q[0][d_var_order[q][i]]; -} - } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 7da5b2088..b96b42dc2 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -42,15 +42,10 @@ namespace quantifiers { class TermDb; -class FirstOrderModelIG; - namespace fmcheck { class FirstOrderModelFmc; }/* CVC4::theory::quantifiers::fmcheck namespace */ -class FirstOrderModelQInt; -class FirstOrderModelAbs; - struct IsStarAttributeId {}; typedef expr::Attribute IsStarAttribute; @@ -94,10 +89,7 @@ class FirstOrderModel : public TheoryModel public: FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name); - virtual FirstOrderModelIG* asFirstOrderModelIG() { return nullptr; } virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; } - virtual FirstOrderModelQInt* asFirstOrderModelQInt() { return nullptr; } - virtual FirstOrderModelAbs* asFirstOrderModelAbs() { return nullptr; } /** assert quantifier */ void assertQuantifier( Node n ); /** get number of asserted quantifiers */ @@ -172,11 +164,11 @@ class FirstOrderModel : public TheoryModel /** get variable id */ std::map > d_quant_var_id; /** process initialize model for term */ - virtual void processInitializeModelForTerm(Node n) = 0; + virtual void processInitializeModelForTerm(Node n) {} /** process initialize quantifier */ virtual void processInitializeQuantifier(Node q) {} /** process initialize */ - virtual void processInitialize(bool ispre) = 0; + virtual void processInitialize(bool ispre) {} private: // list of inactive quantified formulas @@ -193,85 +185,6 @@ class FirstOrderModel : public TheoryModel void computeModelBasisArgAttribute(Node n); };/* class FirstOrderModel */ -class FirstOrderModelIG : public FirstOrderModel -{ - public: // for Theory UF: - /** class for generating models for uninterpreted functions - * - * This implements the model construction from page 6 of Reynolds et al, - * "Quantifier Instantiation Techniques for Finite Model Finding in SMT", - * CADE 2013. - */ - class UfModelTreeGenerator - { - public: - UfModelTreeGenerator() {} - ~UfModelTreeGenerator() {} - /** set default value */ - void setDefaultValue(Node v) { d_default_value = v; } - /** set value */ - void setValue( - TheoryModel* m, Node n, Node v, bool ground = true, bool isReq = true); - /** make model */ - void makeModel(TheoryModel* m, uf::UfModelTree& tree); - /** reset */ - void clear(); - - public: - /** the overall default value */ - Node d_default_value; - /** - * Stores (required, ground) values in key, value pairs of the form - * ( P( a, b ), c ), which indicates P( a, b ) has value c in the model. - * The "non-ground" values indicate that the key has a "model-basis" - * variable, for example, ( P( _, b ), c ) indicates that P( x, b ) has the - * value b for any value of x. - */ - std::map d_set_values[2][2]; - /** stores the set of non-ground keys in the above maps */ - std::vector d_defaults; - /** - * Returns the term corresponding to the intersection of n1 and n2, if it - * exists, for example, for P( _, a ) and P( b, _ ), this method returns - * P( b, a ), where _ is the "model basis" variable. We take into account - * equality between arguments, so if a=b, then the intersection of P( a, a ) - * and P( b, _ ) is P( a, a ). - */ - Node getIntersection(TheoryModel* m, Node n1, Node n2, bool& isGround); - }; - /** models for each UF operator */ - std::map d_uf_model_tree; - /** model generators for each UF operator */ - std::map 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 ); -//the following functions are for evaluating quantifier bodies -public: - FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name); - - FirstOrderModelIG* asFirstOrderModelIG() override { return this; } - // initialize the model - void processInitialize(bool ispre) override; - //for initialize model - void processInitializeModelForTerm(Node n) override; - /** reset evaluation */ - void resetEvaluate(); - /** evaluate functions */ - int evaluate( Node n, int& depIndex, RepSetIterator* ri ); - Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ); -private: - //default evaluate term function - Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ); -};/* class FirstOrderModelIG */ - - namespace fmcheck { class Def; @@ -301,36 +214,6 @@ class FirstOrderModelFmc : public FirstOrderModel }/* CVC4::theory::quantifiers::fmcheck namespace */ -class AbsDef; - -class FirstOrderModelAbs : public FirstOrderModel -{ - public: - std::map< Node, AbsDef * > d_models; - std::map< Node, bool > d_models_valid; - std::map< TNode, unsigned > d_rep_id; - std::map< TypeNode, unsigned > d_domain; - std::map< Node, std::vector< int > > d_var_order; - std::map< Node, std::map< int, int > > d_var_index; - - private: - /** get current model value */ - void processInitializeModelForTerm(Node n) override; - void processInitializeQuantifier(Node q) override; - void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars ); - TNode getUsedRepresentative( TNode n ); - - public: - FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name); - ~FirstOrderModelAbs() override; - FirstOrderModelAbs* asFirstOrderModelAbs() override { return this; } - void processInitialize(bool ispre) override; - unsigned getRepresentativeId( TNode n ); - bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); } - Node getFunctionValue(Node op, const char* argPrefix ); - Node getVariable( Node q, unsigned i ); -}; - }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/fmf/ambqi_builder.cpp b/src/theory/quantifiers/fmf/ambqi_builder.cpp deleted file mode 100644 index f2b131f21..000000000 --- a/src/theory/quantifiers/fmf/ambqi_builder.cpp +++ /dev/null @@ -1,971 +0,0 @@ -/********************* */ -/*! \file ambqi_builder.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of abstract MBQI builder - **/ - -#include "theory/quantifiers/fmf/ambqi_builder.h" - -#include "base/cvc4_check.h" -#include "options/quantifiers_options.h" -#include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" - -using namespace std; -using namespace CVC4::kind; -using namespace CVC4::context; - -namespace CVC4 { -namespace theory { -namespace quantifiers { - - -void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth ) { - d_def.clear(); - Assert( !fapps.empty() ); - if( depth==fapps[0].getNumChildren() ){ - //if( fapps.size()>1 ){ - // for( unsigned i=0; i " << m->getRepresentativeId( fapps[i] ) << std::endl; - // } - //} - //get representative in model for this term - d_value = m->getRepresentativeId( fapps[0] ); - Assert( d_value!=val_none ); - }else{ - TypeNode tn = fapps[0][depth].getType(); - std::map< unsigned, std::vector< TNode > > fapp_child; - - //partition based on evaluations of fapps[1][depth]....fapps[n][depth] - for( unsigned i=0; igetRepresentativeId( fapps[i][depth] ); - Assert( r < 32 ); - fapp_child[r].push_back( fapps[i] ); - } - - //do completion - std::map< unsigned, unsigned > fapp_child_index; - unsigned def = m->d_domain[ tn ]; - unsigned minSize = fapp_child.begin()->second.size(); - unsigned minSizeIndex = fapp_child.begin()->first; - for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){ - fapp_child_index[it->first] = ( 1 << it->first ); - def = def & ~( 1 << it->first ); - if( it->second.size()second.size(); - minSizeIndex = it->first; - } - } - fapp_child_index[minSizeIndex] |= def; - d_default = fapp_child_index[minSizeIndex]; - - //construct children - for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){ - Trace("abs-model-debug") << "Construct " << it->first << " : " << fapp_child_index[it->first] << " : "; - const RepSet* rs = m->getRepSet(); - debugPrintUInt("abs-model-debug", - rs->getNumRepresentatives(tn), - fapp_child_index[it->first]); - Trace("abs-model-debug") << " : " << it->second.size() << " terms." << std::endl; - d_def[fapp_child_index[it->first]].construct_func( m, it->second, depth+1 ); - } - } -} - -void AbsDef::simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth ) { - if( d_value==val_none && !d_def.empty() ){ - //process the default - std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default ); - Assert( defd!=d_def.end() ); - unsigned newDef = d_default; - std::vector< unsigned > to_erase; - defd->second.simplify( m, q, n, depth+1 ); - int defVal = defd->second.d_value; - bool isConstant = ( defVal!=val_none ); - //process each child - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - if( it->first!=d_default ){ - it->second.simplify( m, q, n, depth+1 ); - if( it->second.d_value==defVal && it->second.d_value!=val_none ){ - newDef = newDef | it->first; - to_erase.push_back( it->first ); - }else{ - isConstant = false; - } - } - } - if( !to_erase.empty() ){ - //erase old default - int defVal = defd->second.d_value; - d_def.erase( d_default ); - //set new default - d_default = newDef; - d_def[d_default].construct_def_entry( m, q, n, defVal, depth+1 ); - //erase redundant entries - for( unsigned i=0; igetRepSet(); - unsigned dSize = rs->getNumRepresentatives(tn); - Assert( dSize<32 ); - for( std::map< unsigned, AbsDef >::const_iterator it = d_def.begin(); it != d_def.end(); ++it ){ - for( unsigned i=0; ifirst ); - if( it->first==d_default ){ - Trace(c) << "*"; - } - if( it->second.d_value!=val_none ){ - Trace(c) << " -> V[" << it->second.d_value << "]"; - } - Trace(c) << std::endl; - it->second.debugPrint( c, m, f, depth+1 ); - } - } - } -} - -bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth ) { - if( inst==0 || !options::fmfOneInstPerRound() ){ - if( d_value==1 ){ - //instantiations are all true : ignore this - return true; - }else{ - if( depth==q[0].getNumChildren() ){ - if (qe->getInstantiate()->addInstantiation(q, terms, true)) - { - Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl; - inst++; - return true; - }else{ - Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl; - //we are incomplete - return false; - } - }else{ - bool osuccess = true; - TypeNode tn = m->getVariable( q, depth ).getType(); - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - //get witness term - unsigned index = 0; - bool success; - do { - success = false; - index = getId( it->first, index ); - if( index<32 ){ - const RepSet* rs = m->getRepSet(); - Assert(index < rs->getNumRepresentatives(tn)); - terms[m->d_var_order[q][depth]] = - rs->getRepresentative(tn, index); - if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){ - //if we are incomplete, and have not yet added an instantiation, keep trying - index++; - Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl; - }else{ - success = true; - } - } - }while( !qe->inConflict() && !success && index<32 ); - //mark if we are incomplete - osuccess = osuccess && success; - } - return osuccess; - } - } - }else{ - return true; - } -} - -void AbsDef::construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth ) { - if( depth==entry.size() ){ - d_value = v; - }else{ - d_def[entry[depth]].construct_entry( entry, entry_def, v, depth+1 ); - if( entry_def[depth] ){ - d_default = entry[depth]; - } - } -} - -void AbsDef::get_defs( unsigned u, std::vector< AbsDef * >& defs ) { - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - if( ( u & it->first )!=0 ){ - Assert( (u & it->first)==u ); - defs.push_back( &it->second ); - } - } -} - -void AbsDef::construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< AbsDef * >& defs, unsigned depth ) { - if( depth==q[0].getNumChildren() ){ - Assert( defs.size()==1 ); - d_value = defs[0]->d_value; - }else{ - TypeNode tn = m->getVariable( q, depth ).getType(); - unsigned def = m->d_domain[tn]; - for( unsigned i=0; i::iterator itd = defs[i]->d_def.begin(); itd != defs[i]->d_def.end(); ++itd ){ - if( isSimple( itd->first ) && ( def & itd->first )!=0 ){ - def &= ~( itd->first ); - //process this value - std::vector< AbsDef * > cdefs; - for( unsigned j=0; jget_defs( itd->first, cdefs ); - } - d_def[itd->first].construct_normalize( m, q, cdefs, depth+1 ); - if( def==0 ){ - d_default = itd->first; - break; - } - } - } - if( def==0 ){ - break; - } - } - if( def!=0 ){ - d_default = def; - //process the default - std::vector< AbsDef * > cdefs; - for( unsigned j=0; jget_defs( d_default, cdefs ); - } - d_def[d_default].construct_normalize( m, q, cdefs, depth+1 ); - } - } -} - -void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth ) { - d_value = v; - if( depthgetVariable( q, depth ).getType(); - unsigned dom = m->d_domain[tn] ; - d_def[dom].construct_def_entry( m, q, n, v, depth+1 ); - d_default = dom; - } -} - -void AbsDef::apply_ucompose( FirstOrderModelAbs * m, TNode q, - std::vector< unsigned >& entry, std::vector< bool >& entry_def, - std::vector< int >& terms, std::map< unsigned, int >& vchildren, - AbsDef * a, unsigned depth ) { - if( depth==terms.size() ){ - if( Trace.isOn("ambqi-check-debug2") ){ - Trace("ambqi-check-debug2") << "Add entry ( "; - const RepSet* rs = m->getRepSet(); - for( unsigned i=0; igetNumRepresentatives(m->getVariable(q, i).getType()); - debugPrintUInt( "ambqi-check-debug2", dSize, entry[i] ); - Trace("ambqi-check-debug2") << " "; - } - Trace("ambqi-check-debug2") << ")" << std::endl; - } - a->construct_entry( entry, entry_def, d_value ); - }else{ - unsigned id; - if( terms[depth]==val_none ){ - //a variable - std::map< unsigned, int >::iterator itv = vchildren.find( depth ); - Assert( itv!=vchildren.end() ); - unsigned prev_v = entry[itv->second]; - bool prev_vd = entry_def[itv->second]; - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - entry[itv->second] = it->first & prev_v; - entry_def[itv->second] = ( it->first==d_default ) && prev_vd; - if( entry[itv->second]!=0 ){ - it->second.apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 ); - } - } - entry[itv->second] = prev_v; - entry_def[itv->second] = prev_vd; - }else{ - id = (unsigned)terms[depth]; - Assert( id<32 ); - unsigned fid = 1 << id; - std::map< unsigned, AbsDef >::iterator it = d_def.find( fid ); - if( it!=d_def.end() ){ - it->second.apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 ); - }else{ - d_def[d_default].apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 ); - } - } - } -} - -void AbsDef::construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth ) { - if( depth==q[0].getNumChildren() ){ - Assert( currv!=val_none ); - d_value = currv; - }else{ - TypeNode tn = m->getVariable( q, depth ).getType(); - unsigned dom = m->d_domain[tn]; - int vindex = depth==v1 ? 0 : ( depth==v2 ? 1 : val_none ); - if( vindex==val_none ){ - d_def[dom].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 ); - d_default = dom; - }else{ - Assert( currv==val_none ); - if( curr==val_none ){ - unsigned numReps = m->getRepSet()->getNumRepresentatives(tn); - Assert( numReps < 32 ); - for( unsigned i=0; igetVariable( q, depth ).getType(); - if( v==depth ){ - const unsigned numReps = m->getRepSet()->getNumRepresentatives(tn); - CVC4_CHECK(numReps > 0 && numReps < 32); - for( unsigned i=0; id_domain[tn]; - d_def[dom].construct_var( m, q, v, currv, depth+1 ); - d_default = dom; - } - } -} - -void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, - std::map< unsigned, AbsDef * >& children, - std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren, - std::vector< unsigned >& entry, std::vector< bool >& entry_def ) { - const RepSet* rs = m->getRepSet(); - if( n.getKind()==OR || n.getKind()==AND ){ - // short circuiting - for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ - if( ( it->second->d_value==0 && n.getKind()==AND ) || - ( it->second->d_value==1 && n.getKind()==OR ) ){ - //std::cout << "Short circuit " << it->second->d_value << " " << entry.size() << "/" << q[0].getNumChildren() << std::endl; - unsigned count = q[0].getNumChildren() - entry.size(); - for( unsigned i=0; id_domain[m->getVariable( q, entry.size() ).getType()] ); - entry_def.push_back( true ); - } - construct_entry( entry, entry_def, it->second->d_value ); - for( unsigned i=0; i values; - values.resize( n.getNumChildren(), val_none ); - for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ - values[it->first] = it->second->d_value; - } - for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){ - values[it->first] = it->second; - } - //look up value(s) - f->apply_ucompose( m, q, entry, entry_def, values, vchildren, this ); - }else{ - bool incomplete = false; - //we are composing with an interpreted function - std::vector< TNode > values; - values.resize( n.getNumChildren(), TNode::null() ); - for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ - Trace("ambqi-check-debug2") << "composite : " << it->first << " : " << it->second->d_value; - if( it->second->d_value>=0 ){ - if (it->second->d_value - >= (int)rs->getNumRepresentatives(n[it->first].getType())) - { - std::cout << it->second->d_value << " " << n[it->first] << " " - << n[it->first].getType() << " " - << rs->getNumRepresentatives(n[it->first].getType()) - << std::endl; - } - Assert(it->second->d_value - < (int)rs->getNumRepresentatives(n[it->first].getType())); - values[it->first] = rs->getRepresentative(n[it->first].getType(), - it->second->d_value); - }else{ - incomplete = true; - } - Trace("ambqi-check-debug2") << " ->> " << values[it->first] << std::endl; - } - for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){ - Trace("ambqi-check-debug2") << " basic : " << it->first << " : " << it->second; - if( it->second>=0 ){ - Assert(it->second - < (int)rs->getNumRepresentatives(n[it->first].getType())); - values[it->first] = - rs->getRepresentative(n[it->first].getType(), it->second); - }else{ - incomplete = true; - } - Trace("ambqi-check-debug2") << " ->> " << values[it->first] << std::endl; - } - Assert( vchildren.empty() ); - if( incomplete ){ - Trace("ambqi-check-debug2") << "Construct incomplete entry." << std::endl; - - //if a child is unknown, we must return unknown - construct_entry( entry, entry_def, val_unk ); - }else{ - if( Trace.isOn("ambqi-check-debug2") ){ - for( unsigned i=0; imkNode( n.getKind(), values ); - vv = Rewriter::rewrite( vv ); - int v = m->getRepresentativeId( vv ); - construct_entry( entry, entry_def, v ); - } - } - }else{ - //take product of arguments - TypeNode tn = m->getVariable( q, entry.size() ).getType(); - Assert( m->isValidType( tn ) ); - unsigned def = m->d_domain[tn]; - if( Trace.isOn("ambqi-check-debug2") ){ - for( unsigned i=0; i::iterator it = children.begin(); it != children.end(); ++it ){ - Assert( it->second!=NULL ); - //process each child - for( std::map< unsigned, AbsDef >::iterator itd = it->second->d_def.begin(); itd != it->second->d_def.end(); ++itd ){ - if( itd->first!=it->second->d_default && ( def & itd->first )!=0 ){ - def &= ~( itd->first ); - //process this value - std::map< unsigned, AbsDef * > cchildren; - for( std::map< unsigned, AbsDef * >::iterator it2 = children.begin(); it2 != children.end(); ++it2 ){ - Assert( it2->second!=NULL ); - std::map< unsigned, AbsDef >::iterator itdf = it2->second->d_def.find( itd->first ); - if( itdf!=it2->second->d_def.end() ){ - cchildren[it2->first] = &itdf->second; - }else{ - Assert( it2->second->getDefault()!=NULL ); - cchildren[it2->first] = it2->second->getDefault(); - } - } - if( Trace.isOn("ambqi-check-debug2") ){ - for( unsigned i=0; igetNumRepresentatives(tn), - itd->first); - Trace("ambqi-check-debug2") << " " << children.size() << " " << cchildren.size() << std::endl; - } - entry.push_back( itd->first ); - entry_def.push_back( def==0 ); - construct_compose( m, q, n, f, cchildren, bchildren, vchildren, entry, entry_def ); - entry_def.pop_back(); - entry.pop_back(); - if( def==0 ){ - break; - } - } - } - if( def==0 ){ - break; - } - } - if( def!=0 ){ - if( Trace.isOn("ambqi-check-debug2") ){ - for( unsigned i=0; i cdchildren; - for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ - Assert( it->second->getDefault()!=NULL ); - cdchildren[it->first] = it->second->getDefault(); - } - if( Trace.isOn("ambqi-check-debug2") ){ - for( unsigned i=0; igetNumRepresentatives(tn), def); - Trace("ambqi-check-debug2") << " " << children.size() << " " << cdchildren.size() << std::endl; - } - entry.push_back( def ); - entry_def.push_back( true ); - construct_compose( m, q, n, f, cdchildren, bchildren, vchildren, entry, entry_def ); - entry_def.pop_back(); - entry.pop_back(); - } - } -} - -bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, - std::map< unsigned, AbsDef * >& children, - std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren, - int varChCount ) { - if( Trace.isOn("ambqi-check-debug3") ){ - for( unsigned i=0; i::iterator it = bchildren.begin(); it !=bchildren.end(); ++it ){ - if( ( it->second==0 && n.getKind()==AND ) || - ( it->second==1 && n.getKind()==OR ) ){ - construct_def_entry( m, q, q[0], it->second ); - return true; - } - } - } - Trace("ambqi-check-debug2") << "Construct compose..." << std::endl; - std::vector< unsigned > entry; - std::vector< bool > entry_def; - if( f && varChCount>0 ){ - AbsDef unorm; - unorm.construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def ); - //normalize - std::vector< AbsDef* > defs; - defs.push_back( &unorm ); - construct_normalize( m, q, defs ); - }else{ - construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def ); - } - Assert( is_normalized() ); - return true; - }else if( varChCount==1 && ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) ){ - Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl; - //expand the variable based on its finite domain - AbsDef a; - a.construct_var( m, q, vchildren.begin()->second, val_none ); - children[vchildren.begin()->first] = &a; - vchildren.clear(); - std::vector< unsigned > entry; - std::vector< bool > entry_def; - Trace("ambqi-check-debug2") << "Construct compose with variable..." << std::endl; - construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def ); - return true; - }else if( varChCount==2 && ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) ){ - Trace("ambqi-check-debug2") << "Construct variable equality..." << std::endl; - //efficient expansion of the equality - construct_var_eq( m, q, vchildren[0], vchildren[1], val_none, val_none ); - return true; - }else{ - return false; - } -} - -void AbsDef::negate() { - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - it->second.negate(); - } - if( d_value==0 ){ - d_value = 1; - }else if( d_value==1 ){ - d_value = 0; - } -} - -Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth ) { - const RepSet* rs = m->getRepSet(); - if( depth==vars.size() ){ - TypeNode tn = op.getType(); - if( tn.getNumChildren()>0 ){ - tn = tn[tn.getNumChildren() - 1]; - } - if( d_value>=0 ){ - Assert(d_value < (int)rs->getNumRepresentatives(tn)); - if( tn.isBoolean() ){ - return NodeManager::currentNM()->mkConst( d_value==1 ); - }else{ - return rs->getRepresentative(tn, d_value); - } - }else{ - return Node::null(); - } - }else{ - TypeNode tn = vars[depth].getType(); - Node curr; - curr = d_def[d_default].getFunctionValue( m, op, vars, depth+1 ); - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - if( it->first!=d_default ){ - unsigned id = getId( it->first ); - Assert(id < rs->getNumRepresentatives(tn)); - TNode n = rs->getRepresentative(tn, id); - Node fv = it->second.getFunctionValue( m, op, vars, depth+1 ); - if( !curr.isNull() && !fv.isNull() ){ - curr = NodeManager::currentNM()->mkNode( ITE, vars[depth].eqNode( n ), fv, curr ); - }else{ - curr = Node::null(); - } - } - } - return curr; - } -} - -bool AbsDef::isSimple( unsigned n ) { - return (n & (n - 1))==0; -} - -unsigned AbsDef::getId( unsigned n, unsigned start, unsigned end ) { - Assert( n!=0 ); - while( (n & ( 1 << start )) == 0 ){ - start++; - if( start==end ){ - return start; - } - } - return start; -} - -Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< Node >& args ) { - std::vector< unsigned > iargs; - for( unsigned i=0; igetRepresentativeId( args[i] ); - iargs.push_back( v ); - } - return evaluate( m, retTyp, iargs, 0 ); -} - -Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< unsigned >& iargs, unsigned depth ) { - if( d_value!=val_none ){ - if( d_value==val_unk ){ - return Node::null(); - }else{ - const RepSet* rs = m->getRepSet(); - Assert(d_value >= 0 && d_value < (int)rs->getNumRepresentatives(retTyp)); - return rs->getRepresentative(retTyp, d_value); - } - }else{ - std::map< unsigned, AbsDef >::iterator it = d_def.find( iargs[depth] ); - if( it==d_def.end() ){ - return d_def[d_default].evaluate( m, retTyp, iargs, depth+1 ); - }else{ - return it->second.evaluate( m, retTyp, iargs, depth+1 ); - } - } -} - -bool AbsDef::is_normalized() { - for( std::map< unsigned, AbsDef >::iterator it1 = d_def.begin(); it1 != d_def.end(); ++it1 ){ - if( !it1->second.is_normalized() ){ - return false; - } - for( std::map< unsigned, AbsDef >::iterator it2 = d_def.begin(); it2 != d_def.end(); ++it2 ){ - if( it1->first!=it2->first && (( it1->first & it2->first )!=0) ){ - return false; - } - } - } - return true; -} - -AbsMbqiBuilder::AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ) : -QModelBuilder( c, qe ){ - d_true = NodeManager::currentNM()->mkConst( true ); - d_false = NodeManager::currentNM()->mkConst( false ); -} - - -//------------------------model construction---------------------------- - -bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) { - if (!m->areFunctionValuesEnabled()) - { - // nothing to do if no functions - return true; - } - Trace("ambqi-debug") << "process build model " << std::endl; - FirstOrderModel* f = (FirstOrderModel*)m; - FirstOrderModelAbs* fm = f->asFirstOrderModelAbs(); - RepSet* rs = m->getRepSetPtr(); - fm->initialize(); - //process representatives - fm->d_rep_id.clear(); - fm->d_domain.clear(); - - //initialize boolean sort - TypeNode b = d_true.getType(); - rs->d_type_reps[b].clear(); - rs->d_type_reps[b].push_back(d_false); - rs->d_type_reps[b].push_back(d_true); - fm->d_rep_id[d_false] = 0; - fm->d_rep_id[d_true] = 1; - - //initialize unintpreted sorts - Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl; - for (std::map >::iterator it = - rs->d_type_reps.begin(); - it != rs->d_type_reps.end(); - ++it) - { - if( it->first.isSort() ){ - Assert( !it->second.empty() ); - //set the domain - fm->d_domain[it->first] = 0; - Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl; - for( unsigned i=0; isecond.size(); i++ ){ - if( i<32 ){ - fm->d_domain[it->first] |= ( 1 << i ); - } - Trace("ambqi-model") << i << " : " << it->second[i] << std::endl; - fm->d_rep_id[it->second[i]] = i; - } - if( it->second.size()>=32 ){ - fm->d_domain.erase( it->first ); - } - } - } - - Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl; - //construct the models for functions - for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - Node f = it->first; - Trace("ambqi-model-debug") << "Building Model for " << f << std::endl; - //reset the model - it->second->clear(); - //get all (non-redundant) f-applications - std::vector< TNode > fapps; - Trace("ambqi-model-debug") << "Initial terms: " << std::endl; - std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( f ); - if( itut!=fm->d_uf_terms.end() ){ - for( size_t i=0; isecond.size(); i++ ){ - Node n = itut->second[i]; - // only consider unique up to congruence (in model equality engine)? - Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl; - fapps.push_back( n ); - } - } - if( fapps.empty() ){ - //choose arbitrary value - Node mbt = fm->getModelBasisOpTerm(f); - Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl; - fapps.push_back( mbt ); - } - bool fValid = true; - for( unsigned i=0; id_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){ - Trace("ambqi-model") << "Interpretation of " << f << " is not valid."; - Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl; - fValid = false; - break; - } - } - fm->d_models_valid[f] = fValid; - if( fValid ){ - //construct the ambqi model - it->second->construct_func( fm, fapps ); - Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl; - it->second->debugPrint("ambqi-model-debug", fm, fapps[0] ); - Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl; - it->second->simplify( fm, TNode::null(), fapps[0] ); - Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl; - it->second->debugPrint("ambqi-model", fm, fapps[0] ); - -/* - if( Debug.isOn("ambqi-model-debug") ){ - for( size_t i=0; id_uf_terms[f].size(); i++ ){ - Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] ); - Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl; - Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) ); - } - } -*/ - } - } - Trace("ambqi-model") << "Construct model representation..." << std::endl; - //make function values - for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - if( it->first.getType().getNumChildren()>1 ){ - Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl; - Node f_def = fm->getFunctionValue( it->first, "$x" ); - m->assignFunctionDefinition( it->first, f_def ); - } - } - Assert( d_addedLemmas==0 ); - return TheoryEngineModelBuilder::processBuildModel( m ); -} - - -//--------------------model checking--------------------------------------- - -//do exhaustive instantiation -int AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) { - Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl; - if (effort==0) { - FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs(); - bool quantValid = true; - for( unsigned i=0; iisValidType( q[0][i].getType() ) ){ - quantValid = false; - Trace("ambqi-inst") << "Interpretation of " << q << " is not valid because of type " << q[0][i].getType() << std::endl; - break; - } - } - if( quantValid ){ - Trace("ambqi-check") << "Compute interpretation..." << std::endl; - AbsDef ad; - doCheck( fma, q, ad, q[1] ); - //now process entries - Trace("ambqi-inst-debug") << "...Current : " << d_addedLemmas << std::endl; - Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl; - ad.debugPrint( "ambqi-inst", fma, q[0] ); - Trace("ambqi-inst") << std::endl; - Trace("ambqi-check") << "Add instantiations..." << std::endl; - int lem = 0; - quantValid = ad.addInstantiations( fma, d_qe, q, lem ); - Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl; - if( lem>0 ){ - //if we were incomplete but added at least one lemma, we are ok - quantValid = true; - } - d_addedLemmas += lem; - Trace("ambqi-inst-debug") << "...Total : " << d_addedLemmas << std::endl; - } - return quantValid ? 1 : 0; - }else{ - return 1; - } -} - -bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) { - Assert( n.getKind()!=FORALL ); - if( n.getKind()==NOT && n[0].getKind()!=FORALL ){ - doCheck( m, q, ad, n[0] ); - ad.negate(); - return true; - }else{ - std::map< unsigned, AbsDef > children; - std::map< unsigned, int > bchildren; - std::map< unsigned, int > vchildren; - int varChCount = 0; - for( unsigned i=0; id_var_index[q][ m->getVariableId( q, n[i] ) ]; - //vchildren[i] = m->getVariableId( q, n[i] ); - }else if( m->hasTerm( n[i] ) ){ - bchildren[i] = m->getRepresentativeId( n[i] ); - }else{ - if( !doCheck( m, q, children[i], n[i] ) ){ - bchildren[i] = AbsDef::val_unk; - children.erase( i ); - } - } - } - //convert to pointers - std::map< unsigned, AbsDef * > pchildren; - for( std::map< unsigned, AbsDef >::iterator it = children.begin(); it != children.end(); ++it ){ - pchildren[it->first] = &it->second; - } - //construct the interpretation - Trace("ambqi-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl; - if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){ - Node op; - if( n.getKind() == APPLY_UF ){ - op = n.getOperator(); - }else{ - op = n; - } - //uninterpreted compose - if( m->d_models_valid[op] ){ - ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount ); - }else{ - Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (no function model)" << std::endl; - return false; - } - }else if( !ad.construct( m, q, n, NULL, pchildren, bchildren, vchildren, varChCount ) ){ - Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (variables are children of interpreted symbol)" << std::endl; - return false; - } - Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl; - ad.debugPrint("ambqi-check-try", m, q[0] ); - ad.simplify( m, q, q[0] ); - Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl; - ad.debugPrint("ambqi-check-debug", m, q[0] ); - Trace("ambqi-check-debug") << std::endl; - return true; - } -} - -}/* namespace CVC4::theory::quantifiers */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ diff --git a/src/theory/quantifiers/fmf/ambqi_builder.h b/src/theory/quantifiers/fmf/ambqi_builder.h deleted file mode 100644 index b052e0985..000000000 --- a/src/theory/quantifiers/fmf/ambqi_builder.h +++ /dev/null @@ -1,105 +0,0 @@ -/********************* */ -/*! \file ambqi_builder.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Abstract MBQI model builder class - **/ - -#include "cvc4_private.h" - -#ifndef ABSTRACT_MBQI_BUILDER -#define ABSTRACT_MBQI_BUILDER - -#include "theory/quantifiers/fmf/model_builder.h" -#include "theory/quantifiers/first_order_model.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class FirstOrderModelAbs; - -//representiation of function and term interpretations -class AbsDef -{ -private: - bool addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth ); - void construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, - std::map< unsigned, AbsDef * >& children, - std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren, - std::vector< unsigned >& entry, std::vector< bool >& entry_def ); - void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 ); - void construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth = 0 ); - void apply_ucompose( FirstOrderModelAbs * m, TNode q, - std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms, - std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth = 0 ); - void construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth = 0 ); - void construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int currv, unsigned depth = 0 ); - void get_defs( unsigned u, std::vector< AbsDef * >& defs ); - void construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< AbsDef * >& defs, unsigned depth = 0 ); -public: - enum { - val_none = -1, - val_unk = -2, - }; - AbsDef() : d_default( 0 ), d_value( -1 ){} - std::map< unsigned, AbsDef > d_def; - unsigned d_default; - int d_value; - - void clear() { d_def.clear(); d_default = 0; d_value = -1; } - AbsDef * getDefault() { return &d_def[d_default]; } - void construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth = 0 ); - void debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const; - void debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth = 0 ) const; - void simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth = 0 ); - int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){ - std::vector< Node > terms; - terms.resize( q[0].getNumChildren() ); - return addInstantiations( m, qe, q, terms, inst, 0 ); - } - bool construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, - std::map< unsigned, AbsDef * >& children, - std::map< unsigned, int >& bchildren, - std::map< unsigned, int >& vchildren, - int varChCount ); - void negate(); - Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 ); - static bool isSimple( unsigned n ); - static unsigned getId( unsigned n, unsigned start=0, unsigned end=32 ); - Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args ); - Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 ); - //for debugging - bool is_normalized(); -}; - -class AbsMbqiBuilder : public QModelBuilder -{ - friend class AbsDef; -private: - Node d_true; - Node d_false; - bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ); -public: - AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ); - - //process build model - bool processBuildModel(TheoryModel* m) override; - //do exhaustive instantiation - int doExhaustiveInstantiation(FirstOrderModel* fm, - Node q, - int effort) override; -}; - -} -} -} - -#endif diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index c03fc7a32..8ef30fc4d 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -143,687 +143,3 @@ void QModelBuilder::debugModel( TheoryModel* m ){ } } } - -bool TermArgBasisTrie::addTerm(FirstOrderModel* fm, Node n, unsigned argIndex) -{ - if (argIndex < n.getNumChildren()) - { - Node r; - if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){ - r = n[ argIndex ]; - }else{ - r = fm->getRepresentative( n[ argIndex ] ); - } - std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r ); - if( it==d_data.end() ){ - d_data[r].addTerm(fm, n, argIndex + 1); - return true; - }else{ - return it->second.addTerm(fm, n, argIndex + 1); - } - }else{ - return false; - } -} - -void QModelBuilderIG::UfModelPreferenceData::setValuePreference(Node q, - Node r, - bool isPro) -{ - if (std::find(d_values.begin(), d_values.end(), r) == d_values.end()) - { - d_values.push_back(r); - } - int index = isPro ? 0 : 1; - if (std::find( - d_value_pro_con[index][r].begin(), d_value_pro_con[index][r].end(), q) - == d_value_pro_con[index][r].end()) - { - d_value_pro_con[index][r].push_back(q); - } -} - -Node QModelBuilderIG::UfModelPreferenceData::getBestDefaultValue( - Node defaultTerm, TheoryModel* m) -{ - Node defaultVal; - double maxScore = -1; - for (size_t i = 0, size = d_values.size(); i < size; i++) - { - Node v = d_values[i]; - double score = (1.0 + static_cast(d_value_pro_con[0][v].size())) - / (1.0 + static_cast(d_value_pro_con[1][v].size())); - Debug("fmf-model-cons-debug") << " - score( "; - Debug("fmf-model-cons-debug") << m->getRepresentative(v); - Debug("fmf-model-cons-debug") << " ) = " << score << std::endl; - if (score > maxScore) - { - defaultVal = v; - maxScore = score; - } - } - if (maxScore < 1.0) - { - // consider finding another value, if possible - Debug("fmf-model-cons-debug") - << "Poor choice for default value, score = " << maxScore << std::endl; - TypeNode tn = defaultTerm.getType(); - Node newDefaultVal = m->getRepSet()->getDomainValue(tn, d_values); - if (!newDefaultVal.isNull()) - { - defaultVal = newDefaultVal; - Debug("fmf-model-cons-debug") << "-> Change default value to "; - Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal); - Debug("fmf-model-cons-debug") << std::endl; - } - else - { - Debug("fmf-model-cons-debug") - << "-> Could not find arbitrary element of type " - << tn[tn.getNumChildren() - 1] << std::endl; - Debug("fmf-model-cons-debug") << " Excluding: " << d_values; - Debug("fmf-model-cons-debug") << std::endl; - } - } - // get the default term (this term must be defined non-ground in model) - Debug("fmf-model-cons-debug") << " Choose "; - Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal); - Debug("fmf-model-cons-debug") - << " as default value (" << defaultTerm << ")" << std::endl; - Debug("fmf-model-cons-debug") - << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() - << std::endl; - Debug("fmf-model-cons-debug") - << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() - << std::endl; - return defaultVal; -} - -QModelBuilderIG::QModelBuilderIG(context::Context* c, QuantifiersEngine* qe) - : QModelBuilder(c, qe), - d_didInstGen(false), - d_numQuantSat(0), - d_numQuantInstGen(0), - d_numQuantNoInstGen(0), - d_numQuantNoSelForm(0), - d_instGenMatches(0) {} - -/* -Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) { - return n; -} -*/ - -bool QModelBuilderIG::processBuildModel( TheoryModel* m ) { - if (!m->areFunctionValuesEnabled()) - { - // nothing to do if no functions - return true; - } - FirstOrderModel* f = (FirstOrderModel*)m; - FirstOrderModelIG* fm = f->asFirstOrderModelIG(); - Trace("model-engine-debug") << "Process build model " << optUseModel() << std::endl; - d_didInstGen = false; - //reset the internal information - reset( fm ); - //only construct first order model if optUseModel() is true - if( optUseModel() ){ - Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl; - //check if any quantifiers are un-initialized - for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ - Node q = fm->getAssertedQuantifier( i ); - if( d_qe->getModel()->isQuantifierActive( q ) ){ - int lems = initializeQuantifier(q, q, f); - d_statistics.d_init_inst_gen_lemmas += lems; - d_addedLemmas += lems; - if( d_qe->inConflict() ){ - break; - } - } - } - if( d_addedLemmas>0 ){ - Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl; - return false; - }else{ - Assert( !d_qe->inConflict() ); - //initialize model - fm->initialize(); - //analyze the functions - Trace("model-engine-debug") << "Analyzing model..." << std::endl; - analyzeModel( fm ); - //analyze the quantifiers - Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl; - d_uf_prefs.clear(); - for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ - Node q = fm->getAssertedQuantifier( i ); - analyzeQuantifier( fm, q ); - } - - //if applicable, find exceptions to model via inst-gen - if( options::fmfInstGen() ){ - d_didInstGen = true; - d_instGenMatches = 0; - d_numQuantSat = 0; - d_numQuantInstGen = 0; - d_numQuantNoInstGen = 0; - d_numQuantNoSelForm = 0; - //now, see if we know that any exceptions via InstGen exist - Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl; - for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - if( d_qe->getModel()->isQuantifierActive( f ) ){ - int lems = doInstGen( fm, f ); - d_statistics.d_inst_gen_lemmas += lems; - d_addedLemmas += lems; - //temporary - if( lems>0 ){ - d_numQuantInstGen++; - }else if( hasInstGen( f ) ){ - d_numQuantNoInstGen++; - }else{ - d_numQuantNoSelForm++; - } - if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){ - break; - } - }else{ - d_numQuantSat++; - } - } - Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / "; - Trace("model-engine-debug") << d_numQuantNoInstGen << " / " << d_numQuantNoSelForm << std::endl; - Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches << 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; - } - } - } - //construct the model if necessary - 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; - //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 ){ - Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl; - constructModelUf( fm, it->first ); - } - Trace("model-engine-debug") << "Done building models." << std::endl; - }else{ - return false; - } - } - } - //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 ); - Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl; - //construct function values - Node f_def = it->second.getFunctionValue( "$x" ); - fm->assignFunctionDefinition( it->first, f_def ); - } - Assert( d_addedLemmas==0 ); - return TheoryEngineModelBuilder::processBuildModel( m ); -} - -int QModelBuilderIG::initializeQuantifier(Node f, Node fp, FirstOrderModel* fm) -{ - if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){ - //create the basis match if necessary - if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){ - Trace("inst-fmf-init") << "Initialize " << f << std::endl; - //add the model basis instantiation - // This will help produce the necessary information for model completion. - // We do this by extending distinguish ground assertions (those - // containing terms with "model basis" attribute) to hold for all cases. - - ////first, check if any variables are required to be equal - //for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin(); - // it != d_quantEngine->d_phase_reqs[f].end(); ++it ){ - // Node n = it->first; - // if( n.getKind()==EQUAL && n[0].getKind()==INST_CONSTANT && n[1].getKind()==INST_CONSTANT ){ - // Notice() << "Unhandled phase req: " << n << std::endl; - // } - //} - d_quant_basis_match[f] = InstMatch( f ); - for (unsigned j = 0; j < f[0].getNumChildren(); j++) - { - Node t = fm->getModelBasisTerm(f[0][j].getType()); - //calculate the basis match for f - d_quant_basis_match[f].setValue( j, t ); - } - ++(d_statistics.d_num_quants_init); - } - //try to add it - Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl; - //add model basis instantiation - if (d_qe->getInstantiate()->addInstantiation(fp, d_quant_basis_match[f])) - { - d_quant_basis_match_added[f] = true; - 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_quant_basis_match_added[f] = false; - } - } - return 0; -} - -void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ - FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); - d_uf_model_constructed.clear(); - //determine if any functions are constant - for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){ - Node op = it->first; - std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op ); - if( itut!=fmig->d_uf_terms.end() ){ - for( size_t i=0; isecond.size(); i++ ){ - Node n = fmig->d_uf_terms[op][i]; - //for calculating if op is constant - Node v = fmig->getRepresentative( n ); - if( i==0 ){ - d_uf_prefs[op].d_const_val = v; - }else if( v!=d_uf_prefs[op].d_const_val ){ - d_uf_prefs[op].d_const_val = Node::null(); - break; - } - } - } - if( !d_uf_prefs[op].d_const_val.isNull() ){ - fmig->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val ); - fmig->d_uf_model_gen[op].makeModel( fmig, it->second ); - Debug("fmf-model-cons") << "Function " << op << " is the constant function "; - Debug("fmf-model-cons") << d_uf_prefs[op].d_const_val; - Debug("fmf-model-cons") << std::endl; - d_uf_model_constructed[op] = true; - }else{ - d_uf_model_constructed[op] = false; - } - } -} - -bool QModelBuilderIG::hasConstantDefinition( Node n ){ - Node lit = n.getKind()==NOT ? n[0] : n; - if( lit.getKind()==APPLY_UF ){ - Node op = lit.getOperator(); - if( !d_uf_prefs[op].d_const_val.isNull() ){ - return true; - } - } - return false; -} - -QModelBuilderIG::Statistics::Statistics() - : d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0), - d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", - 0), - d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0), - d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0) -{ - smtStatisticsRegistry()->registerStat(&d_num_quants_init); - smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init); - smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas); - smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas); -} - -QModelBuilderIG::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_num_quants_init); - smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init); - smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas); -} - -//do exhaustive instantiation -int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { - if( optUseModel() ){ - QRepBoundExt qrbe(d_qe); - RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe); - if( riter.setQuantifier( f ) ){ - FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel(); - Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl; - fmig->resetEvaluate(); - Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; - EqualityQuery* qy = d_qe->getEqualityQuery(); - Instantiate* inst = d_qe->getInstantiate(); - TermUtil* util = d_qe->getTermUtil(); - while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ - d_triedLemmas++; - if( Debug.isOn("inst-fmf-ei-debug") ){ - for( int i=0; i<(int)riter.d_index.size(); i++ ){ - Debug("inst-fmf-ei-debug") << i << " : " << riter.d_index[i] << " : " << riter.getCurrentTerm( i ) << std::endl; - } - } - int eval = 0; - int depIndex; - //see if instantiation is already true in current model - if( Debug.isOn("fmf-model-eval") ){ - Debug("fmf-model-eval") << "Evaluating "; - riter.debugPrintSmall("fmf-model-eval"); - Debug("fmf-model-eval") << "Done calculating terms." << std::endl; - } - //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; - Debug("fmf-model-eval") << "We will evaluate " - << util->getInstConstantBody(f) << std::endl; - eval = fmig->evaluate(util->getInstConstantBody(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 ){ - //instantiation is already true -> skip - riter.incrementAtIndex(depIndex); - }else{ - //instantiation was not shown to be true, construct the match - InstMatch m( f ); - for (unsigned i = 0; i < riter.getNumTerms(); i++) - { - m.set(qy, i, riter.getCurrentTerm(i)); - } - Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; - //add as instantiation - if (inst->addInstantiation(f, m, true)) - { - d_addedLemmas++; - if( d_qe->inConflict() ){ - break; - } - //if the instantiation is show to be false, and we wish to skip multiple instantiations at once - if( eval==-1 ){ - riter.incrementAtIndex(depIndex); - }else{ - riter.increment(); - } - }else{ - Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; - riter.increment(); - } - } - } - //print debugging information - Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl; - Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas << std::endl; - Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas << std::endl; - if( d_addedLemmas>1000 ){ - Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl; - Trace("model-engine-warn") << " Inst Tried: " << d_triedLemmas << std::endl; - Trace("model-engine-warn") << " Inst Added: " << d_addedLemmas << std::endl; - Trace("model-engine-warn") << std::endl; - } - } - //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round - return riter.isIncomplete() ? -1 : 1; - }else{ - return 0; - } -} - - - -void QModelBuilderDefault::reset( FirstOrderModel* fm ){ - 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(); -} - - -int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) { - /* - size_t maxChildren = 0; - for( size_t i=0; imaxChildren ){ - maxChildren = uf_terms[i].getNumChildren(); - } - } - //TODO: look at how many entries they have? - return (int)maxChildren; - */ - return 0; -} - -void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ - if( d_qe->getModel()->isQuantifierActive( f ) ){ - FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); - 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; - Trace("inst-gen-debug-quant") << "Inst-gen analyze " << f << std::endl; - //for each asserted quantifier f, - // - determine selection literals - // - check which function/predicates have good and bad definitions for satisfying f - if( d_phase_reqs.find( f )==d_phase_reqs.end() ){ - d_phase_reqs[f].initialize( d_qe->getTermUtil()->getInstConstantBody( f ), true ); - } - int selectLitScore = -1; - for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){ - //the literal n is phase-required for quantifier f - Node n = it->first; - Node gn = fm->getModelBasis(f, 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( TermUtil::hasInstConstAttr(n) ){ - isConst = false; - if( gn.getKind()==APPLY_UF ){ - uf_terms.push_back( gn ); - isConst = hasConstantDefinition( gn ); - }else if( gn.getKind()==EQUAL ){ - isConst = true; - for( int j=0; j<2; j++ ){ - if( TermUtil::hasInstConstAttr(n[j]) ){ - if( n[j].getKind()==APPLY_UF && - fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){ - uf_terms.push_back( gn[j] ); - isConst = isConst && hasConstantDefinition( gn[j] ); - }else{ - isConst = false; - } - } - } - } - } - //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_qe->getModel()->isQuantifierActive( f ); - d_qe->getModel()->setQuantifierActive( f, false ); - //check if choosing this literal would add any additional constraints to default definitions - selectLitConstraints = false; - selectLit = true; - } - //also check if it is naturally a better literal - if( !selectLit ){ - int score = getSelectionScore( uf_terms ); - //Trace("inst-gen-debug") << "Check " << score << " < " << selectLitScore << std::endl; - selectLit = scoregetModel()->isQuantifierActive( f ) ){ - 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] ); - } - } - } - } - //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" << std::endl; - } - //process information about requirements and preferences of quantifier f - if( !d_qe->getModel()->isQuantifierActive( f ) ){ - 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] << " "; - } - Debug("fmf-model-prefs") << std::endl; - }else{ - //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 = fmig->getRepresentative( pro_con[k][j] ); - d_uf_prefs[op].setValuePreference(f, r, k == 0); - } - } - } - } -} - -int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ - 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. - if( !d_quant_selection_lit[f].isNull() ){ - Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl; - for( size_t i=0; i tr_terms; - if( lit.getKind()==APPLY_UF ){ - //only match predicates that are contrary to this one, use literal matching - Node eq = NodeManager::currentNM()->mkNode( - EQUAL, lit, NodeManager::currentNM()->mkConst(!phase)); - tr_terms.push_back( eq ); - }else if( lit.getKind()==EQUAL ){ - //collect trigger terms - for( int j=0; j<2; j++ ){ - if( TermUtil::hasInstConstAttr(lit[j]) ){ - 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, true, inst::Trigger::TR_MAKE_NEW ); - //Notice() << "Trigger = " << (*tr) << std::endl; - tr->resetInstantiationRound(); - tr->reset( Node::null() ); - //d_qe->d_optInstMakeRepresentative = false; - //d_qe->d_optMatchIgnoreModelBasis = true; - addedLemmas += tr->addInstantiations(); - } - } - } - return addedLemmas; -} - -void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ - FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); - if( !d_uf_model_constructed[op] ){ - //construct the model for the uninterpretted function/predicate - bool setDefaultVal = true; - Node defaultTerm = fmig->getModelBasisOpTerm(op); - Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl; - //set the values in the model - std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op ); - if( itut!=fmig->d_uf_terms.end() ){ - for( size_t i=0; isecond.size(); i++ ){ - Node n = itut->second[i]; - // only consider unique up to congruence (in model equality engine)? - Node v = fmig->getRepresentative( n ); - Trace("fmf-model-cons") << "Set term " << n << " : " - << fmig->getRepSet()->getIndexFor(v) << " " << v - << std::endl; - //if this assertion did not help the model, just consider it ground - //set n = v in the model tree - //set it as ground value - fmig->d_uf_model_gen[op].setValue( fm, n, v ); - // also set as default value if necessary - if (n.hasAttribute(ModelBasisArgAttribute()) - && n.getAttribute(ModelBasisArgAttribute()) != 0) - { - Trace("fmf-model-cons") << " Set as default." << std::endl; - fmig->d_uf_model_gen[op].setValue(fm, n, v, false); - if( n==defaultTerm ){ - //incidentally already set, we will not need to find a default value - setDefaultVal = false; - } - } - } - } - //set the overall default value if not set already (is this necessary??) - if( setDefaultVal ){ - Trace("fmf-model-cons") << " Choose default value..." << std::endl; - //chose defaultVal based on heuristic, currently the best ratio of "pro" responses - Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); - if( defaultVal.isNull() ){ - if (!fmig->getRepSet()->hasType(defaultTerm.getType())) - { - Node mbt = fmig->getModelBasisTerm(defaultTerm.getType()); - fmig->getRepSetPtr()->d_type_reps[defaultTerm.getType()].push_back( - mbt); - } - defaultVal = - fmig->getRepSet()->getRepresentative(defaultTerm.getType(), 0); - } - Assert( !defaultVal.isNull() ); - Trace("fmf-model-cons") - << "Set default term : " << fmig->getRepSet()->getIndexFor(defaultVal) - << std::endl; - fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); - } - Debug("fmf-model-cons") << " Making model..."; - fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] ); - d_uf_model_constructed[op] = true; - Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl; - } -} diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index b34f1e580..b73716169 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -56,163 +56,6 @@ public: unsigned getNumTriedLemmas() { return d_triedLemmas; } }; -class TermArgBasisTrie { -public: - /** the data */ - std::map< Node, TermArgBasisTrie > d_data; - /** add term to the trie */ - bool addTerm(FirstOrderModel* fm, Node n, unsigned argIndex = 0); -};/* class TermArgBasisTrie */ - -/** model builder class - * This class is capable of building candidate models based on the current quantified formulas - * that are asserted. Use: - * (1) call QModelBuilder::buildModel( m, false );, where m is a FirstOrderModel - * (2) if candidate model is determined to be a real model, - then call QModelBuilder::buildModel( m, true ); - */ -class QModelBuilderIG : public QModelBuilder -{ - typedef context::CDHashMap BoolMap; - - protected: - /** - * This class stores temporary information useful to model engine for - * constructing models for uninterpreted functions. - */ - class UfModelPreferenceData - { - public: - UfModelPreferenceData() {} - virtual ~UfModelPreferenceData() {} - /** any constant value of the type */ - Node d_const_val; - /** list of possible default values */ - std::vector d_values; - /** - * Map from values to the set of quantified formulas that are (pro, con) - * that value. A quantified formula may be "pro" a particular default - * value of an uninterpreted function if that value is likely to satisfy - * many points in its domain. For example, forall x. P( f( x ) ) may be - * "pro" the default value true for P. - */ - std::map > d_value_pro_con[2]; - /** set that quantified formula q is pro/con the default value of r */ - void setValuePreference(Node q, Node r, bool isPro); - /** get best default value */ - Node getBestDefaultValue(Node defaultTerm, TheoryModel* m); - }; - /** map from operators to model preference data */ - std::map d_uf_prefs; - //built model uf - std::map< Node, bool > d_uf_model_constructed; - //whether inst gen was done - bool d_didInstGen; - /** process build model */ - bool processBuildModel(TheoryModel* m) override; - - protected: - //reset - virtual void reset( FirstOrderModel* fm ) = 0; - //initialize quantifiers, return number of lemmas produced - virtual int initializeQuantifier(Node f, Node fp, FirstOrderModel* fm); - //analyze model - virtual void analyzeModel( FirstOrderModel* fm ); - //analyze quantifiers - virtual void analyzeQuantifier( FirstOrderModel* fm, Node f ) = 0; - //do InstGen techniques for quantifier, return number of lemmas produced - virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0; - //theory-specific build models - virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0; - - protected: - //map from quantifiers to if are SAT - //std::map< Node, bool > d_quant_sat; - //which quantifiers have been initialized - std::map< Node, bool > d_quant_basis_match_added; - //map from quantifiers to model basis match - std::map< Node, InstMatch > d_quant_basis_match; - - protected: // helper functions - /** term has constant definition */ - bool hasConstantDefinition( Node n ); - - public: - QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ); - - public: - /** statistics class */ - class Statistics { - public: - IntStat d_num_quants_init; - IntStat d_num_partial_quants_init; - IntStat d_init_inst_gen_lemmas; - IntStat d_inst_gen_lemmas; - Statistics(); - ~Statistics(); - }; - Statistics d_statistics; - // is term selected - virtual bool isTermSelected( Node n ) { return false; } - /** quantifier has inst-gen definition */ - virtual bool hasInstGen( Node f ) = 0; - /** did inst gen this round? */ - bool didInstGen() { return d_didInstGen; } - // is quantifier active? - bool isQuantifierActive( Node f ); - //do exhaustive instantiation - int doExhaustiveInstantiation(FirstOrderModel* fm, - Node f, - int effort) override; - - //temporary stats - int d_numQuantSat; - int d_numQuantInstGen; - int d_numQuantNoInstGen; - int d_numQuantNoSelForm; - //temporary stat - int d_instGenMatches; -};/* class QModelBuilder */ - - -class QModelBuilderDefault : public QModelBuilderIG -{ - private: /// information for (old) InstGen - // 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; - //get selection score - int getSelectionScore( std::vector< Node >& uf_terms ); - - protected: - //reset - void reset(FirstOrderModel* fm) override; - //analyze quantifier - void analyzeQuantifier(FirstOrderModel* fm, Node f) override; - //do InstGen techniques for quantifier, return number of lemmas produced - int doInstGen(FirstOrderModel* fm, Node f) override; - //theory-specific build models - void constructModelUf(FirstOrderModel* fm, Node op) override; - - protected: - std::map< Node, QuantPhaseReq > d_phase_reqs; - - public: - QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){} - - //has inst gen - bool hasInstGen(Node f) override - { - return !d_quant_selection_lit[f].isNull(); - } -}; - }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 81ecf9e77..d2579b4ee 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -15,7 +15,6 @@ #include "theory/quantifiers/fmf/model_engine.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/fmf/ambqi_builder.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/instantiate.h" diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 320f50afb..433621d31 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -30,7 +30,6 @@ #include "theory/quantifiers/equality_infer.h" #include "theory/quantifiers/equality_query.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/fmf/ambqi_builder.h" #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/fmf/model_engine.h" @@ -249,20 +248,14 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc")); d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this)); - }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ - Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl; - d_model.reset( - new quantifiers::FirstOrderModelAbs(this, c, "FirstOrderModelAbs")); - d_builder.reset(new quantifiers::AbsMbqiBuilder(c, this)); }else{ Trace("quant-engine-debug") << "...make default model builder." << std::endl; d_model.reset( - new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG")); - d_builder.reset(new quantifiers::QModelBuilderDefault(c, this)); + new quantifiers::FirstOrderModel(this, c, "FirstOrderModel")); + d_builder.reset(new quantifiers::QModelBuilder(c, this)); } }else{ - d_model.reset( - new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG")); + d_model.reset(new quantifiers::FirstOrderModel(this, c, "FirstOrderModel")); } } diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index a3e058569..42847dfd4 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -37,17 +37,6 @@ void UfModelTreeNode::clear(){ d_value = Node::null(); } -bool UfModelTreeNode::hasConcreteArgumentDefinition(){ - if( d_data.size()>1 ){ - return true; - }else if( d_data.empty() ){ - return false; - }else{ - Node r; - return d_data.find( r )==d_data.end(); - } -} - //set value function void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){ if( d_data.empty() ){ @@ -67,75 +56,6 @@ void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int } } -//get value function -Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){ - if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){ - //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl; - depIndex = argIndex; - return d_value; - }else{ - Node val; - int childDepIndex[2] = { argIndex, argIndex }; - for( int i=0; i<2; i++ ){ - //first check the argument, then check default - Node r; - if( i==0 ){ - r = m->getRepresentative( n[ indexOrder[argIndex] ] ); - } - std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); - if( it!=d_data.end() ){ - val = it->second.getValue( m, n, indexOrder, childDepIndex[i], argIndex+1 ); - if( !val.isNull() ){ - break; - } - }else{ - //argument is not a defined argument: thus, it depends on this argument - childDepIndex[i] = argIndex+1; - } - } - //update depIndex - depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1]; - //Notice() << "Return " << val << ", depIndex = " << depIndex; - //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl; - return val; - } -} - -Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){ - if( argIndex==(int)indexOrder.size() ){ - return d_value; - }else{ - Node val; - bool depArg = false; - //will try concrete value first, then default - for( int i=0; i<2; i++ ){ - Node r; - if( i==0 ){ - r = m->getRepresentative( n[ indexOrder[argIndex] ] ); - } - std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); - if( it!=d_data.end() ){ - val = it->second.getValue( m, n, indexOrder, depIndex, argIndex+1 ); - //we have found a value - if( !val.isNull() ){ - if( i==0 ){ - depArg = true; - } - break; - } - } - } - //it depends on this argument if we found it via concrete argument value, - // or if found by default/disequal from some concrete argument value(s). - if( depArg || hasConcreteArgumentDefinition() ){ - if( std::find( depIndex.begin(), depIndex.end(), indexOrder[argIndex] )==depIndex.end() ){ - depIndex.push_back( indexOrder[argIndex] ); - } - } - return val; - } -} - Node UfModelTreeNode::getFunctionValue(std::vector& args, int index, Node argDefaultValue, bool simplify) { if(!d_data.empty()) { Node defaultValue = argDefaultValue; @@ -264,10 +184,6 @@ bool UfModelTreeNode::isTotal( Node op, int argIndex ){ } } -Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){ - return d_value; -} - void indent( std::ostream& out, int ind ){ for( int i=0; i d_data; /** the value of this tree node (if all paths lead to same value) */ Node d_value; - /** has concrete argument defintion */ - bool hasConcreteArgumentDefinition(); public: //is this model tree empty? bool isEmpty() { return d_data.empty() && d_value.isNull(); } @@ -40,11 +38,6 @@ public: void clear(); /** setValue function */ void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ); - /** getValue function */ - Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ); - Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ); - /** getConstant Value function */ - Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ); /** getFunctionValue */ Node getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue, bool simplify = true ); /** update function */ @@ -92,36 +85,6 @@ public: void setDefaultValue( TheoryModel* m, Node v ){ d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 ); } - /** getValue function - * - * returns val, the value of ground term n - * Say n is f( t_0...t_n ) - * depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to val - * for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c, - * then g( a, a, a ) would return b with depIndex = 1 - * - */ - Node getValue( TheoryModel* m, Node n, int& depIndex ){ - return d_tree.getValue( m, n, d_index_order, depIndex, 0 ); - } - /** -> implementation incomplete */ - Node getValue( TheoryModel* m, Node n, std::vector< int >& depIndex ){ - return d_tree.getValue( m, n, d_index_order, depIndex, 0 ); - } - /** getConstantValue function - * - * given term n, where n may contain "all value" arguments, aka model basis arguments - * if n is null, then every argument of n is considered "all value" - * if n is constant for the entire domain specified by n, then this function returns the value of its domain - * otherwise, it returns null - * for example, say the term e represents "all values" - * if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b, - * then f( a, e ) would return b, while f( e, a ) would return null - * -> implementation incomplete - */ - Node getConstantValue( TheoryModel* m, Node n ) { - return d_tree.getConstantValue( m, n, d_index_order, 0 ); - } /** getFunctionValue * Returns a representation of this function. */ @@ -136,8 +99,6 @@ public: void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); } /** is this tree total? */ bool isTotal() { return d_tree.isTotal( d_op, 0 ); } - /** is this function constant? */ - bool isConstant( TheoryModel* m ) { return !getConstantValue( m, Node::null() ).isNull(); } /** is this tree empty? */ bool isEmpty() { return d_tree.isEmpty(); } public: diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt index e8c7949dc..bb2630b93 100644 --- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt +++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --mbqi=gen-ev +; COMMAND-LINE: --finite-model-find ; EXPECT: unsat (benchmark Isabelle :status sat diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smt b/test/regress/regress0/fmf/QEpres-uf.855035.smt index 4fe592638..97a585090 100644 --- a/test/regress/regress0/fmf/QEpres-uf.855035.smt +++ b/test/regress/regress0/fmf/QEpres-uf.855035.smt @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --mbqi=gen-ev +; COMMAND-LINE: --finite-model-find ; EXPECT: sat (benchmark Isabelle :status sat diff --git a/test/regress/regress1/fmf/nlp042+1.smt2 b/test/regress/regress1/fmf/nlp042+1.smt2 index 567a3c0b7..6159f0b41 100644 --- a/test/regress/regress1/fmf/nlp042+1.smt2 +++ b/test/regress/regress1/fmf/nlp042+1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --mbqi=abs --no-check-models +; COMMAND-LINE: --finite-model-find --no-check-models ; EXPECT: sat (set-logic UF) (set-info :status sat)