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
\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\
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\
";
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") {
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;
};
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,
};
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 );
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
#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"
return n.getAttribute(ModelBasisArgAttribute());
}
-Node FirstOrderModelIG::UfModelTreeGenerator::getIntersection(TheoryModel* m,
- Node n1,
- Node n2,
- bool& isGround)
-{
- isGround = true;
- std::vector<Node> 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<Node, Node>::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( childDepIndex<posDepIndex ){
- posDepIndex = childDepIndex;
- if( posDepIndex==-1 ){
- break;
- }
- }
- }else if( eValT==0 ){
- if( eVal==baseVal ){
- eVal = 0;
- }
- }
- }
- if( eVal!=0 ){
- depIndex = eVal==-baseVal ? posDepIndex : negDepIndex;
- return eVal;
- }else{
- return 0;
- }
- }else if( n.getKind()==EQUAL && n[0].getType().isBoolean() ){
- int depIndex1;
- int eVal = evaluate( n[0], depIndex1, ri );
- if( eVal!=0 ){
- int depIndex2;
- int eVal2 = evaluate( n[1], depIndex2, ri );
- if( eVal2!=0 ){
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- return eVal==eVal2 ? 1 : -1;
- }
- }
- return 0;
- }else if( n.getKind()==ITE ){
- int depIndex1, depIndex2;
- int eVal = evaluate( n[0], depIndex1, ri );
- if( eVal==0 ){
- //evaluate children to see if they are the same value
- int eval1 = evaluate( n[1], depIndex1, ri );
- if( eval1!=0 ){
- int eval2 = evaluate( n[1], depIndex2, ri );
- if( eval1==eval2 ){
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- return eval1;
- }
- }
- }else{
- int eValT = evaluate( n[eVal==1 ? 1 : 2], depIndex2, ri );
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- return eValT;
- }
- return 0;
- }else if( n.getKind()==FORALL ){
- return 0;
- }else{
- //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; i<argDepIndex; i++ ){
- int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];
- Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;
- if( children_depIndex[index]>depIndex ){
- depIndex = children_depIndex[index];
- }
- }
- setVal = true;
- }else{
- 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)<getMaxVariableNum(j));}
-};
-
-void FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){
- if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
- //sort arguments in order of least significant vs. most significant variable in default ordering
- std::map< Node, std::vector< int > > argIndex;
- std::vector< Node > args;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( argIndex.find( n[i] )==argIndex.end() ){
- args.push_back( n[i] );
- }
- argIndex[n[i]].push_back( i );
- }
- sortGetMaxVariableNum sgmvn;
- std::sort( args.begin(), args.end(), sgmvn );
- for( int i=0; i<(int)args.size(); i++ ){
- for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){
- d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] );
- }
- }
- bool useDefault = true;
- for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
- if( i!=d_eval_term_index_order[n][i] ){
- useDefault = false;
- break;
- }
- }
- d_eval_uf_use_default[n] = useDefault;
- Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : ";
- for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
- Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " ";
- }
- Debug("fmf-index-order") << std::endl;
- }
-}
-
FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :
FirstOrderModel(qe, c, name){
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<Node, AbsDef*>::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<Node, AbsDef * >::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<tno.getNumChildren(); i++) {
- //make sure a representative of the type exists
- if( !d_rep_set.hasType( tno[i] ) ){
- Node e = getSomeDomainElement( tno[i] );
- Trace("ambqi-debug") << " * Initialize type " << tno[i] << ", add ";
- Trace("ambqi-debug") << e << " " << e.getType() << std::endl;
- //d_rep_set.add( e );
- }
- }
- }
- }
-}
-
-unsigned FirstOrderModelAbs::getRepresentativeId( TNode n ) {
- TNode r = getUsedRepresentative( n );
- std::map< TNode, unsigned >::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; i<type.getNumChildren()-1; i++ ){
- std::stringstream ss;
- ss << argPrefix << (i+1);
- Node b = NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] );
- vars.push_back( b );
- }
- Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
- Node curr = d_models[op]->getFunctionValue( this, 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<n.getNumChildren(); i++ ){
- if( n.getKind()==EQUAL && n[i].getKind()==BOUND_VARIABLE ){
- int v = getVariableId( q, n[i] );
- Assert( v>=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<q[0].getNumChildren(); i++ ){
- eq_vars[i] = false;
- }
- collectEqVars( q, q[1], eq_vars );
- for( unsigned r=0; r<2; r++ ){
- for( std::map< int, bool >::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 */
class TermDb;
-class FirstOrderModelIG;
-
namespace fmcheck {
class FirstOrderModelFmc;
}/* CVC4::theory::quantifiers::fmcheck namespace */
-class FirstOrderModelQInt;
-class FirstOrderModelAbs;
-
struct IsStarAttributeId {};
typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
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 */
/** get variable id */
std::map<Node, std::map<Node, int> > 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
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<Node, Node> d_set_values[2][2];
- /** stores the set of non-ground keys in the above maps */
- std::vector<Node> 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<Node, uf::UfModelTree> d_uf_model_tree;
- /** model generators for each UF operator */
- std::map<Node, UfModelTreeGenerator> d_uf_model_gen;
-
- private:
- //map from terms to the models used to calculate their value
- std::map< Node, bool > d_eval_uf_use_default;
- std::map< Node, uf::UfModelTree > d_eval_uf_model;
- void makeEvalUfModel( Node n );
- //index ordering to use for each term
- std::map< Node, std::vector< int > > d_eval_term_index_order;
- void makeEvalUfIndexOrder( Node n );
-//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;
}/* 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 */
+++ /dev/null
-/********************* */
-/*! \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<fapps.size(); i++ ){
- // std::cout << "...." << fapps[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; i<fapps.size(); i++ ){
- unsigned r = m->getRepresentativeId( 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()<minSize ){
- minSize = it->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; i<to_erase.size(); i++ ){
- d_def.erase( to_erase[i] );
- }
- }
- //if constant, propagate the value upwards
- if( isConstant ){
- d_value = defVal;
- }else{
- d_value = val_none;
- }
- }
-}
-
-void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const{
- for( unsigned i=0; i<dSize; i++ ){
- Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
- }
- //Trace(c) << "(";
- //for( unsigned i=0; i<32; i++ ){
- // Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
- //}
- //Trace(c) << ")";
-}
-
-void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth ) const{
- if( Trace.isOn(c) ){
- if( depth==f.getNumChildren() ){
- for( unsigned i=0; i<depth; i++ ){ Trace(c) << " ";}
- Trace(c) << "V[" << d_value << "]" << std::endl;
- }else{
- TypeNode tn = f[depth].getType();
- const RepSet* rs = m->getRepSet();
- 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; i<depth; i++ ){ Trace(c) << " ";}
- debugPrintUInt( c, dSize, it->first );
- 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<defs.size(); i++ ){
- //process each simple child
- for( std::map< unsigned, AbsDef >::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; j<defs.size(); j++ ){
- defs[j]->get_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; j<defs.size(); j++ ){
- defs[j]->get_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( depth<n.getNumChildren() ){
- TypeNode tn = q.isNull() ? n[depth].getType() : m->getVariable( 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; i<entry.size(); i++ ){
- unsigned dSize =
- rs->getNumRepresentatives(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; i<numReps; i++ ){
- curr = 1 << i;
- d_def[curr].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 );
- }
- d_default = curr;
- }else{
- d_def[curr].construct_var_eq( m, q, v1, v2, curr, 1, depth+1 );
- dom = dom & ~curr;
- d_def[dom].construct_var_eq( m, q, v1, v2, curr, 0, depth+1 );
- d_default = dom;
- }
- }
- }
-}
-
-void AbsDef::construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int currv, unsigned depth ) {
- if( depth==q[0].getNumChildren() ){
- Assert( currv!=val_none );
- d_value = currv;
- }else{
- TypeNode tn = m->getVariable( q, depth ).getType();
- if( v==depth ){
- const unsigned numReps = m->getRepSet()->getNumRepresentatives(tn);
- CVC4_CHECK(numReps > 0 && numReps < 32);
- for( unsigned i=0; i<numReps; i++ ){
- d_def[ 1 << i ].construct_var( m, q, v, i, depth+1 );
- }
- d_default = 1 << (numReps - 1);
- }else{
- unsigned dom = m->d_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; i<count; i++ ){
- entry.push_back( m->d_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<count; i++ ){
- entry.pop_back();
- entry_def.pop_back();
- }
- return;
- }
- }
- }
- if( entry.size()==q[0].getNumChildren() ){
- if( f ){
- if( Trace.isOn("ambqi-check-debug2") ){
- for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }
- Trace("ambqi-check-debug2") << "Evaluate uninterpreted function entry..." << std::endl;
- }
- //we are composing with an uninterpreted function
- std::vector< int > 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; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }
- Trace("ambqi-check-debug2") << "Evaluate interpreted function entry ( ";
- for( unsigned i=0; i<values.size(); i++ ){
- Assert( !values[i].isNull() );
- Trace("ambqi-check-debug2") << values[i] << " ";
- }
- Trace("ambqi-check-debug2") << ")..." << std::endl;
- }
- //evaluate
- Node vv = NodeManager::currentNM()->mkNode( 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<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }
- Trace("ambqi-check-debug2") << "Take product of arguments" << std::endl;
- }
- for( std::map< unsigned, AbsDef * >::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; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }
- Trace("ambqi-check-debug2") << "...process : ";
- debugPrintUInt("ambqi-check-debug2",
- rs->getNumRepresentatives(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<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }
- Trace("ambqi-check-debug2") << "Make default argument" << std::endl;
- }
- std::map< unsigned, AbsDef * > 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; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }
- Trace("ambqi-check-debug2") << "...process default : ";
- debugPrintUInt(
- "ambqi-check-debug2", rs->getNumRepresentatives(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<n.getNumChildren(); i++ ){
- Trace("ambqi-check-debug3") << i << " : ";
- Trace("ambqi-check-debug3") << ((children.find( i )!=children.end()) ? "X" : ".");
- if( bchildren.find( i )!=bchildren.end() ){
- Trace("ambqi-check-debug3") << bchildren[i];
- }else{
- Trace("ambqi-check-debug3") << ".";
- }
- if( vchildren.find( i )!=vchildren.end() ){
- Trace("ambqi-check-debug3") << vchildren[i];
- }else{
- Trace("ambqi-check-debug3") << ".";
- }
- Trace("ambqi-check-debug3") << std::endl;
- }
- Trace("ambqi-check-debug3") << "varChCount : " << varChCount << std::endl;
- }
- if( varChCount==0 || f ){
- //short-circuit
- if( n.getKind()==AND || n.getKind()==OR ){
- for( std::map< unsigned, int >::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; i<args.size(); i++ ){
- unsigned v = 1 << m->getRepresentativeId( 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<TypeNode, std::vector<Node> >::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; i<it->second.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<Node, AbsDef * >::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; i<itut->second.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; i<fapps[0].getNumChildren(); i++ ){
- if( fm->d_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; i<fm->d_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<Node, AbsDef * >::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; i<q[0].getNumChildren(); i++ ){
- if( !fma->isValidType( 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; i<n.getNumChildren(); i++ ){
- if( n[i].getKind()==FORALL ){
- bchildren[i] = AbsDef::val_unk;
- }else if( n[i].getKind() == BOUND_VARIABLE ){
- varChCount++;
- vchildren[i] = m->d_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 */
+++ /dev/null
-/********************* */
-/*! \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
}
}
}
-
-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<double>(d_value_pro_con[0][v].size()))
- / (1.0 + static_cast<double>(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; i<fm->getNumAssertedQuantifiers(); 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; i<fm->getNumAssertedQuantifiers(); 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; i<fm->getNumAssertedQuantifiers(); 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; i<itut->second.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; i<uf_terms.size(); i++ ){
- if( uf_terms[i].getNumChildren()>maxChildren ){
- 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 = score<selectLitScore;
- }
- //see if we wish to choose this as a selection literal
- d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() );
- if( selectLit ){
- selectLitScore = getSelectionScore( uf_terms );
- Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl;
- Trace("inst-gen-debug") << " flags: " << isConst << " " << selectLitConstraints << " " << selectLitScore << std::endl;
- d_quant_selection_lit[f] = value ? n : n.notNode();
- selectionLitTerms.clear();
- selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() );
- if( !selectLitConstraints ){
- break;
- }
- }
- pref = 1;
- }else{
- pref = -1;
- }
- //if we are not yet SAT, so we will add to preferences
- if( d_qe->getModel()->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<d_quant_selection_lit_candidates[f].size(); i++ ){
- bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT;
- Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i];
- Assert( TermUtil::hasInstConstAttr(lit) );
- std::vector< Node > tr_terms;
- if( lit.getKind()==APPLY_UF ){
- //only match predicates that are contrary to this one, use literal matching
- Node eq = NodeManager::currentNM()->mkNode(
- 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; i<itut->second.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;
- }
-}
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<Node, bool, NodeHashFunction> 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<Node> 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<Node, std::vector<Node> > 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<Node, UfModelPreferenceData> 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 */
#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"
#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"
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"));
}
}
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() ){
}
}
-//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<Node>& args, int index, Node argDefaultValue, bool simplify) {
if(!d_data.empty()) {
Node defaultValue = argDefaultValue;
}
}
-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<ind; i++ ){
out << " ";
std::map< Node, UfModelTreeNode > 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(); }
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 */
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.
*/
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:
-; COMMAND-LINE: --finite-model-find --mbqi=gen-ev
+; COMMAND-LINE: --finite-model-find
; EXPECT: unsat
(benchmark Isabelle
:status sat
-; COMMAND-LINE: --finite-model-find --mbqi=gen-ev
+; COMMAND-LINE: --finite-model-find
; EXPECT: sat
(benchmark Isabelle
:status sat
-; 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)
projects / cvc5.git / commitdiff