support the get-value and get-model commands
option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
+option dumpModels --dump-models bool :default false
+ output models after every SAT/INVALID/UNKNOWN response
option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
turn on proof generation
# this is just a placeholder for later; it doesn't show up in command-line options listings
Assert(!done());
TNode assertion = get();
- if( options::finiteModelFind() ){
+ if( d_quantEngine && d_quantEngine->getBoundedIntegers() ){
d_quantEngine->getBoundedIntegers()->assertNode(assertion);
}
#include "theory/quantifiers/bounded_integers.h"\r
#include "theory/quantifiers/quant_util.h"\r
#include "theory/quantifiers/first_order_model.h"\r
+#include "theory/quantifiers/model_engine.h"\r
\r
using namespace CVC4;\r
using namespace std;\r
//add initial split lemma\r
Node ltr = NodeManager::currentNM()->mkNode( LT, d_range, NodeManager::currentNM()->mkConst( Rational(0) ) );\r
ltr = Rewriter::rewrite( ltr );\r
- Trace("bound-integers-lemma") << " *** bound int: initial split on " << ltr << std::endl;\r
+ Trace("bound-int-lemma") << " *** bound int: initial split on " << ltr << std::endl;\r
d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );\r
Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;\r
d_range_literal[-1] = ltr_lit;\r
d_lit_to_range[ltr_lit] = -1;\r
d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT;\r
//register with bounded integers\r
- Trace("bound-integers-debug") << "Literal " << ltr_lit << " is literal for " << d_range << std::endl;\r
+ Trace("bound-int-debug") << "Literal " << ltr_lit << " is literal for " << d_range << std::endl;\r
d_bi->addLiteralFromRange(ltr_lit, d_range);\r
}\r
\r
bool pol = n.getKind()!=NOT;\r
Node nlit = n.getKind()==NOT ? n[0] : n;\r
if( d_lit_to_range.find( nlit )!=d_lit_to_range.end() ){\r
- Trace("bound-integers-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")";\r
- Trace("bound-integers-assert") << ", found literal " << nlit;\r
- Trace("bound-integers-assert") << ", it is bound literal " << d_lit_to_range[nlit] << " for " << d_range << std::endl;\r
+ Trace("bound-int-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")";\r
+ Trace("bound-int-assert") << ", found literal " << nlit;\r
+ Trace("bound-int-assert") << ", it is bound literal " << d_lit_to_range[nlit] << " for " << d_range << std::endl;\r
d_range_assertions[nlit] = (pol==d_lit_to_pol[nlit]);\r
if( pol!=d_lit_to_pol[nlit] ){\r
//check if we need a new split?\r
}\r
}else{\r
if (!d_has_range || d_lit_to_range[nlit]<d_curr_range ){\r
- Trace("bound-integers-bound") << "Successfully bound " << d_range << " to " << d_lit_to_range[nlit] << std::endl;\r
+ Trace("bound-int-bound") << "Successfully bound " << d_range << " to " << d_lit_to_range[nlit] << std::endl;\r
d_curr_range = d_lit_to_range[nlit];\r
}\r
//set the range\r
void BoundedIntegers::RangeModel::allocateRange() {\r
d_curr_max++;\r
int newBound = d_curr_max;\r
- Trace("bound-integers-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;\r
+ Trace("bound-int-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;\r
//TODO: newBound should be chosen in a smarter way\r
Node ltr = NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) );\r
ltr = Rewriter::rewrite( ltr );\r
- Trace("bound-integers-lemma") << " *** bound int: split on " << ltr << std::endl;\r
+ Trace("bound-int-lemma") << " *** bound int: split on " << ltr << std::endl;\r
d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );\r
Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;\r
d_range_literal[newBound] = ltr_lit;\r
if (!d_lit_to_pol[it->first]) {\r
rn = rn.negate();\r
}\r
- Trace("bound-integers-dec") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl;\r
+ Trace("bound-int-dec") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl;\r
return rn;\r
}\r
}\r
\r
bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {\r
if( b.getKind()==BOUND_VARIABLE ){\r
- if( isBound( f, b ) ){\r
+ if( !isBound( f, b ) ){\r
return true;\r
}\r
}else{\r
if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){\r
std::map< Node, Node > msum;\r
if (QuantArith::getMonomialSumLit( lit, msum )){\r
- Trace("bound-integers-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;\r
+ Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;\r
for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){\r
- Trace("bound-integers-debug") << " ";\r
+ Trace("bound-int-debug") << " ";\r
if( !it->second.isNull() ){\r
- Trace("bound-integers-debug") << it->second;\r
+ Trace("bound-int-debug") << it->second;\r
if( !it->first.isNull() ){\r
- Trace("bound-integers-debug") << " * ";\r
+ Trace("bound-int-debug") << " * ";\r
}\r
}\r
if( !it->first.isNull() ){\r
- Trace("bound-integers-debug") << it->first;\r
+ Trace("bound-int-debug") << it->first;\r
}\r
- Trace("bound-integers-debug") << std::endl;\r
+ Trace("bound-int-debug") << std::endl;\r
}\r
- Trace("bound-integers-debug") << std::endl;\r
+ Trace("bound-int-debug") << std::endl;\r
for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){\r
- if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE ){\r
+ if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( f, it->first ) ){\r
Node veq;\r
if( QuantArith::isolate( it->first, msum, veq, GEQ ) ){\r
Node n1 = veq[0];\r
}\r
veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );\r
}\r
- Trace("bound-integers-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;\r
+ Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;\r
Node bv = n1.getKind()==BOUND_VARIABLE ? n1 : n2;\r
if( !isBound( f, bv ) ){\r
if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) {\r
- Trace("bound-integers-debug") << "The bound is relevant." << std::endl;\r
+ Trace("bound-int-debug") << "The bound is relevant." << std::endl;\r
d_bounds[n1.getKind()==BOUND_VARIABLE ? 0 : 1][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);\r
}\r
}\r
}\r
\r
void BoundedIntegers::registerQuantifier( Node f ) {\r
- Trace("bound-integers") << "Register quantifier " << f << std::endl;\r
+ Trace("bound-int") << "Register quantifier " << f << std::endl;\r
bool hasIntType = false;\r
+ std::map< Node, int > numMap;\r
for( unsigned i=0; i<f[0].getNumChildren(); i++) {\r
+ numMap[f[0][i]] = i;\r
if( f[0][i].getType().isInteger() ){\r
hasIntType = true;\r
- break;\r
}\r
}\r
if( hasIntType ){\r
if( !isBound(f,v) ){\r
if( d_bounds[1][f].find(v)!=d_bounds[1][f].end() ){\r
d_set[f].push_back(v);\r
+ d_set_nums[f].push_back(numMap[v]);\r
success = true;\r
}\r
}\r
}\r
}while( success );\r
- Trace("bound-integers") << "Bounds are : " << std::endl;\r
+ Trace("bound-int") << "Bounds are : " << std::endl;\r
for( unsigned i=0; i<d_set[f].size(); i++) {\r
Node v = d_set[f][i];\r
Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] );\r
d_range[f][v] = Rewriter::rewrite( r );\r
- Trace("bound-integers") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;\r
+ Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;\r
}\r
if( d_set[f].size()==f[0].getNumChildren() ){\r
d_bound_quants.push_back( f );\r
for( unsigned i=0; i<d_set[f].size(); i++) {\r
Node v = d_set[f][i];\r
Node r = d_range[f][v];\r
+ if( quantifiers::TermDb::hasBoundVarAttr(r) ){\r
+ //introduce a new bound\r
+ Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" );\r
+ /*\r
+ std::vector< Node > bvs;\r
+ quantifiers::TermDb::getBoundVars(r, bvs);\r
+ Assert(bvs.size()>0);\r
+ Node body = NodeManager::currentNM()->mkNode( LEQ, r, new_range );\r
+ std::vector< Node > children;\r
+ //get all the other bounds\r
+ for( unsigned j=0; j<bvs.size(); j++) {\r
+ Node l = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst(Rational(0)), bvs[j]);\r
+ Node u = NodeManager::currentNM()->mkNode( LEQ, bvs[j], d_range[f][bvs[j]] );\r
+ children.push_back(l);\r
+ children.push_back(u);\r
+ }\r
+ Node antec = NodeManager::currentNM()->mkNode( AND, children );\r
+ body = NodeManager::currentNM()->mkNode( IMPLIES, antec, body );\r
+\r
+ Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );\r
+\r
+ Node lem = NodeManager::currentNM()->mkNode( FORALL, bvl, body );\r
+ Trace("bound-int") << "For " << v << ", the quantified formula " << lem << " will be used to minimize the bound." << std::endl;\r
+ Trace("bound-int-lemma") << " *** bound int: bounding quantified lemma " << lem << std::endl;\r
+ d_quantEngine->getOutputChannel().lemma( lem );\r
+ */\r
+ d_nground_range[f][v] = d_range[f][v];\r
+ d_range[f][v] = new_range;\r
+ r = new_range;\r
+ }\r
if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){\r
+ Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl;\r
d_ranges.push_back( r );\r
d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() );\r
d_rms[r]->initialize();\r
}\r
\r
void BoundedIntegers::assertNode( Node n ) {\r
- Trace("bound-integers-assert") << "Assert " << n << std::endl;\r
+ Trace("bound-int-assert") << "Assert " << n << std::endl;\r
Node nlit = n.getKind()==NOT ? n[0] : n;\r
if( d_lit_to_ranges.find(nlit)!=d_lit_to_ranges.end() ){\r
- Trace("bound-integers-assert") << "This is the bounding literal for " << d_lit_to_ranges[nlit].size() << " ranges." << std::endl;\r
+ Trace("bound-int-assert") << "This is the bounding literal for " << d_lit_to_ranges[nlit].size() << " ranges." << std::endl;\r
for( unsigned i=0; i<d_lit_to_ranges[nlit].size(); i++) {\r
Node r = d_lit_to_ranges[nlit][i];\r
- Trace("bound-integers-assert") << " ...this is a bounding literal for " << r << std::endl;\r
+ Trace("bound-int-assert") << " ...this is a bounding literal for " << r << std::endl;\r
d_rms[r]->assertNode( n );\r
}\r
}\r
}\r
\r
Node BoundedIntegers::getNextDecisionRequest() {\r
- Trace("bound-integers-dec") << "bi: Get next decision request?" << std::endl;\r
+ Trace("bound-int-dec") << "bi: Get next decision request?" << std::endl;\r
for( unsigned i=0; i<d_ranges.size(); i++) {\r
Node d = d_rms[d_ranges[i]]->getNextDecisionRequest();\r
if (!d.isNull()) {\r
return Node::null();\r
}\r
\r
+void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {\r
+ l = d_bounds[0][f][v];\r
+ u = d_bounds[1][f][v];\r
+ if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){\r
+ //must create substitution\r
+ std::vector< Node > vars;\r
+ std::vector< Node > subs;\r
+ Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl;\r
+ for( unsigned i=0; i<d_set[f].size(); i++) {\r
+ if( d_set[f][i]!=v ){\r
+ Trace("bound-int-rsi") << "Look up the value for " << d_set[f][i] << " " << rsi->d_var_order[d_set_nums[f][i]] << std::endl;\r
+ Trace("bound-int-rsi") << "term : " << rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]]) << std::endl;\r
+ vars.push_back(d_set[f][i]);\r
+ subs.push_back(rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]]));\r
+ }else{\r
+ break;\r
+ }\r
+ }\r
+ Trace("bound-int-rsi") << "Do substitution..." << std::endl;\r
+ //check if it has been instantiated\r
+ if (!vars.empty() && !d_bnd_it[f][v].hasInstantiated(subs)){\r
+ //must add the lemma\r
+ Node nn = d_nground_range[f][v];\r
+ nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );\r
+ Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[f][v] );\r
+ Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;\r
+ d_quantEngine->getOutputChannel().lemma(lem);\r
+ l = Node::null();\r
+ u = Node::null();\r
+ return;\r
+ }else{\r
+ u = u.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );\r
+ l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );\r
+ }\r
+ }\r
+ Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;\r
+ l = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), l );\r
+ u = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), u );\r
+ Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;\r
+ return;\r
+}\r
\r
-Node BoundedIntegers::getValueInModel( Node n ) {\r
- return d_quantEngine->getModel()->getValue( n );\r
+bool BoundedIntegers::isGroundRange(Node f, Node v) {\r
+ return isBoundVar(f,v) && !quantifiers::TermDb::hasBoundVarAttr(getLowerBound(f,v)) && !quantifiers::TermDb::hasBoundVarAttr(getUpperBound(f,v));\r
}
\ No newline at end of file
\r
namespace CVC4 {\r
namespace theory {\r
+\r
+class RepSetIterator;\r
+\r
namespace quantifiers {\r
\r
+\r
class BoundedIntegers : public QuantifiersModule\r
{\r
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;\r
bool hasNonBoundVar( Node f, Node b );\r
std::map< Node, std::map< Node, Node > > d_bounds[2];\r
std::map< Node, std::vector< Node > > d_set;\r
+ std::map< Node, std::vector< int > > d_set_nums;\r
std::map< Node, std::map< Node, Node > > d_range;\r
+ std::map< Node, std::map< Node, Node > > d_nground_range;\r
void hasFreeVar( Node f, Node n );\r
void process( Node f, Node n, bool pol );\r
void processLiteral( Node f, Node lit, bool pol );\r
void assertNode(Node n);\r
Node getNextDecisionRequest();\r
};\r
- Node getValueInModel( Node n );\r
private:\r
//information for minimizing ranges\r
std::vector< Node > d_ranges;\r
std::map< Node, std::vector< Node > > d_lit_to_ranges;\r
//list of currently asserted arithmetic literals\r
NodeBoolMap d_assertions;\r
+private:\r
+ //class to store whether bounding lemmas have been added\r
+ class BoundInstTrie\r
+ {\r
+ public:\r
+ std::map< Node, BoundInstTrie > d_children;\r
+ bool hasInstantiated( std::vector< Node > & vals, int index = 0, bool madeNew = false ){\r
+ if( index>=(int)vals.size() ){\r
+ return !madeNew;\r
+ }else{\r
+ Node n = vals[index];\r
+ if( d_children.find(n)==d_children.end() ){\r
+ madeNew = true;\r
+ }\r
+ return d_children[n].hasInstantiated(vals,index+1,madeNew);\r
+ }\r
+ }\r
+ };\r
+ std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;\r
private:\r
void addLiteralFromRange( Node lit, Node r );\r
public:\r
void registerQuantifier( Node f );\r
void assertNode( Node n );\r
Node getNextDecisionRequest();\r
+ bool isBoundVar( Node f, Node v ) { return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end(); }\r
+ unsigned getNumBoundVars( Node f ) { return d_set[f].size(); }\r
+ Node getBoundVar( Node f, int i ) { return d_set[f][i]; }\r
+ int getBoundVarNum( Node f, int i ) { return d_set_nums[f][i]; }\r
Node getLowerBound( Node f, Node v ){ return d_bounds[0][f][v]; }\r
Node getUpperBound( Node f, Node v ){ return d_bounds[1][f][v]; }\r
- Node getLowerBoundValue( Node f, Node v ){ return getValueInModel( d_bounds[0][f][v] ); }\r
- Node getUpperBoundValue( Node f, Node v ){ return getValueInModel( d_bounds[1][f][v] ); }\r
+ void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );\r
+ bool isGroundRange(Node f, Node v);\r
};\r
\r
}\r
using namespace CVC4::theory::inst;
bool CandidateGenerator::isLegalCandidate( Node n ){
- return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute()) ) );
+ return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n) ) );
}
void CandidateGeneratorQueue::addCandidate( Node n ) {
int computeMaxVariableNum( Node n ){
if( n.getKind()==INST_CONSTANT ){
return n.getAttribute(InstVarNumAttribute());
- }else if( n.hasAttribute(InstConstantAttribute()) ){
+ }else if( TermDb::hasInstConstAttr(n) ){
int maxVal = -1;
for( int i=0; i<(int)n.getNumChildren(); i++ ){
int val = getMaxVariableNum( n[i] );
}\r
}\r
\r
-Node Def::evaluate( FullModelChecker * m, std::vector<Node> inst ) {\r
+Node Def::evaluate( FullModelChecker * m, std::vector<Node>& inst ) {\r
int gindex = d_et.getGeneralizationIndex(m, inst);\r
if (gindex!=-1) {\r
return d_value[gindex];\r
}\r
}\r
\r
-int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst ) {\r
+int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst ) {\r
return d_et.getGeneralizationIndex(m, inst);\r
}\r
\r
d_et.reset();\r
for (unsigned i=0; i<d_status.size(); i++) {\r
if( d_status[i]!=status_redundant ){\r
- addEntry(m, d_cond[i], d_value[i]);\r
+ addEntry(m, cond[i], value[i]);\r
}\r
}\r
d_status.clear();\r
\r
bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) {\r
Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;\r
- if (effort==0) {\r
- //register the quantifier\r
- if (d_quant_cond.find(f)==d_quant_cond.end()) {\r
- std::vector< TypeNode > types;\r
- for(unsigned i=0; i<f[0].getNumChildren(); i++){\r
- types.push_back(f[0][i].getType());\r
- d_quant_var_id[f][f[0][i]] = i;\r
- }\r
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );\r
- Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );\r
- d_quant_cond[f] = op;\r
- }\r
-\r
- //model check the quantifier\r
- doCheck(fm, f, d_quant_models[f], f[1]);\r
- Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;\r
- d_quant_models[f].debugPrint("fmc", Node::null(), this);\r
- Trace("fmc") << std::endl;\r
- //consider all entries going to false\r
- for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {\r
- if( d_quant_models[f].d_value[i]!=d_true) {\r
- Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;\r
- bool hasStar = false;\r
- std::vector< Node > inst;\r
- for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {\r
- if (isStar(d_quant_models[f].d_cond[i][j])) {\r
- hasStar = true;\r
- inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));\r
- }else{\r
- inst.push_back(d_quant_models[f].d_cond[i][j]);\r
- }\r
+ if (!options::fmfModelBasedInst()) {\r
+ return false;\r
+ }else{\r
+ if (effort==0) {\r
+ //register the quantifier\r
+ if (d_quant_cond.find(f)==d_quant_cond.end()) {\r
+ std::vector< TypeNode > types;\r
+ for(unsigned i=0; i<f[0].getNumChildren(); i++){\r
+ types.push_back(f[0][i].getType());\r
+ d_quant_var_id[f][f[0][i]] = i;\r
}\r
- bool addInst = true;\r
- if( hasStar ){\r
- //try obvious (specified by inst)\r
- Node ev = d_quant_models[f].evaluate(this, inst);\r
- if (ev==d_true) {\r
- addInst = false;\r
- }\r
- }else{\r
- //for debugging\r
- if (Trace.isOn("fmc-test-inst")) {\r
- Node ev = d_quant_models[f].evaluate(this, inst);\r
- if( ev==d_true ){\r
- std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;\r
- exit(0);\r
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );\r
+ Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );\r
+ d_quant_cond[f] = op;\r
+ }\r
+\r
+ //model check the quantifier\r
+ doCheck(fm, f, d_quant_models[f], f[1]);\r
+ Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;\r
+ d_quant_models[f].debugPrint("fmc", Node::null(), this);\r
+ Trace("fmc") << std::endl;\r
+ //consider all entries going to false\r
+ for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {\r
+ if( d_quant_models[f].d_value[i]!=d_true) {\r
+ Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;\r
+ bool hasStar = false;\r
+ std::vector< Node > inst;\r
+ for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {\r
+ if (isStar(d_quant_models[f].d_cond[i][j])) {\r
+ hasStar = true;\r
+ inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));\r
}else{\r
- Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;\r
+ inst.push_back(d_quant_models[f].d_cond[i][j]);\r
}\r
}\r
- }\r
- if( addInst ){\r
- InstMatch m;\r
- for( unsigned j=0; j<inst.size(); j++) {\r
- m.set( d_qe, f, j, inst[j] );\r
+ bool addInst = true;\r
+ if( hasStar ){\r
+ //try obvious (specified by inst)\r
+ Node ev = d_quant_models[f].evaluate(this, inst);\r
+ if (ev==d_true) {\r
+ addInst = false;\r
+ }\r
+ }else{\r
+ //for debugging\r
+ if (Trace.isOn("fmc-test-inst")) {\r
+ Node ev = d_quant_models[f].evaluate(this, inst);\r
+ if( ev==d_true ){\r
+ std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;\r
+ exit(0);\r
+ }else{\r
+ Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;\r
+ }\r
+ }\r
}\r
- if( d_qe->addInstantiation( f, m ) ){\r
- lemmas++;\r
+ if( addInst ){\r
+ InstMatch m;\r
+ for( unsigned j=0; j<inst.size(); j++) {\r
+ m.set( d_qe, f, j, inst[j] );\r
+ }\r
+ if( d_qe->addInstantiation( f, m ) ){\r
+ lemmas++;\r
+ }else{\r
+ //this can happen if evaluation is unknown\r
+ //might try it next effort level\r
+ d_star_insts[f].push_back(i);\r
+ }\r
}else{\r
- //this can happen if evaluation is unknown\r
//might try it next effort level\r
d_star_insts[f].push_back(i);\r
}\r
- }else{\r
- //might try it next effort level\r
- d_star_insts[f].push_back(i);\r
}\r
}\r
- }\r
- }else{\r
- if (!d_star_insts[f].empty()) {\r
- Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;\r
- Trace("fmc-exh") << "Definition was : " << std::endl;\r
- d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);\r
- Trace("fmc-exh") << std::endl;\r
- Def temp;\r
- //simplify the exceptions?\r
- for( int i=(d_star_insts[f].size()-1); i>=0; i--) {\r
- //get witness for d_star_insts[f][i]\r
- int j = d_star_insts[f][i];\r
- if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){\r
- int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );\r
- if( lem==-1 ){\r
- //something went wrong, resort to exhaustive instantiation\r
- return false;\r
- }else{\r
- lemmas += lem;\r
+ }else{\r
+ if (!d_star_insts[f].empty()) {\r
+ Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;\r
+ Trace("fmc-exh") << "Definition was : " << std::endl;\r
+ d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);\r
+ Trace("fmc-exh") << std::endl;\r
+ Def temp;\r
+ //simplify the exceptions?\r
+ for( int i=(d_star_insts[f].size()-1); i>=0; i--) {\r
+ //get witness for d_star_insts[f][i]\r
+ int j = d_star_insts[f][i];\r
+ if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){\r
+ int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );\r
+ if( lem==-1 ){\r
+ //something went wrong, resort to exhaustive instantiation\r
+ return false;\r
+ }else{\r
+ lemmas += lem;\r
+ }\r
}\r
}\r
}\r
}\r
+ return true;\r
}\r
- return true;\r
}\r
\r
int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) {\r
int addedLemmas = 0;\r
- RepSetIterator riter( &(fm->d_rep_set) );\r
+ RepSetIterator riter( d_qe, &(fm->d_rep_set) );\r
Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";\r
debugPrintCond("fmc-exh", c, true);\r
Trace("fmc-exh")<< std::endl;\r
- if( riter.setQuantifier( d_qe, f ) ){\r
+ if( riter.setQuantifier( f ) ){\r
std::vector< RepDomain > dom;\r
for (unsigned i=0; i<c.getNumChildren(); i++) {\r
TypeNode tn = c[i].getType();\r
}\r
curr = Rewriter::rewrite( curr );\r
return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);\r
+}\r
+\r
+Node FullModelChecker::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {\r
+ Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;\r
+ for(unsigned i=0; i<args.size(); i++) {\r
+ args[i] = getRepresentative(fm, args[i]);\r
+ }\r
+ if( n.getKind()==VARIABLE ){\r
+ Node r = getRepresentative(fm, n);\r
+ return r;\r
+ }else if( n.getKind()==APPLY_UF ){\r
+ getModel(fm, n.getOperator());\r
+ return d_models[n.getOperator()]->evaluate(this, args);\r
+ }else{\r
+ return Node::null();\r
+ }\r
}
\ No newline at end of file
d_has_simplified = false;\r
}\r
bool addEntry( FullModelChecker * m, Node c, Node v);\r
- Node evaluate( FullModelChecker * m, std::vector<Node> inst );\r
- int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst );\r
+ Node evaluate( FullModelChecker * m, std::vector<Node>& inst );\r
+ int getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst );\r
void simplify( FullModelChecker * m );\r
void debugPrint(const char * tr, Node op, FullModelChecker * m);\r
};\r
\r
/** process build model */\r
void processBuildModel(TheoryModel* m, bool fullModel);\r
+ /** get current model value */\r
+ Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial );\r
};\r
\r
}\r
InstGenProcess::InstGenProcess( Node n ) : d_node( n ){
- Assert( n.hasAttribute(InstConstantAttribute()) );
+ Assert( TermDb::hasInstConstAttr(n) );
int count = 0;
for( size_t i=0; i<n.getNumChildren(); i++ ){
- if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){
+ if( n[i].getKind()!=INST_CONSTANT && TermDb::hasInstConstAttr(n[i]) ){
d_children.push_back( InstGenProcess( n[i] ) );
d_children_index.push_back( i );
d_children_map[ i ] = count;
if (Trace.isOn("inst-match-warn")) {
// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){
- Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl;
+ Trace("inst-match-warn") << quantifiers::TermDb::getInstConstAttr(var) << std::endl;
Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
}
}
InstMatchGenerator::InstMatchGenerator( Node pat, int matchPolicy ) : d_matchPolicy( matchPolicy ){
d_active_add = false;
- Assert( pat.hasAttribute(InstConstantAttribute()) );
+ Assert( quantifiers::TermDb::hasInstConstAttr(pat) );
d_pattern = pat;
d_match_pattern = pat;
d_next = NULL;
d_match_pattern = d_pattern[0];
}
if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
- if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ||
+ if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) ||
d_match_pattern[0].getKind()==INST_CONSTANT ){
- Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) );
+ Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) );
Node mp = d_match_pattern[1];
//swap sides
Node pat = d_pattern;
}
d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern;
d_match_pattern = mp;
- }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ||
+ }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) ||
d_match_pattern[1].getKind()==INST_CONSTANT ){
- Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) );
+ Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) );
if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching
d_match_pattern = d_match_pattern[0];
}else if( d_match_pattern[1].getKind()==INST_CONSTANT ){
}
int childMatchPolicy = MATCH_GEN_DEFAULT;
for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
- if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
+ if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){
if( d_match_pattern[i].getKind()!=INST_CONSTANT && !Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
InstMatchGenerator * cimg = new InstMatchGenerator( d_match_pattern[i], childMatchPolicy );
d_children.push_back( cimg );
d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
}else{
d_cg = new CandidateGeneratorQueue;
- if( !Trigger::isArithmeticTrigger( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){
+ if( !Trigger::isArithmeticTrigger( quantifiers::TermDb::getInstConstAttr(d_match_pattern), d_match_pattern, d_arith_coeffs ) ){
Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
//Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
InstMatch prev( &m );
//if t is null
Assert( !t.isNull() );
- Assert( !t.hasAttribute(InstConstantAttribute()) );
+ Assert( !quantifiers::TermDb::hasInstConstAttr(t) );
Assert( t.getKind()==d_match_pattern.getKind() );
Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );
//first, check if ground arguments are not equal, or a match is in conflict
for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
- if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
+ if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){
if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
Node vv = d_match_pattern[i];
Node tt = t[i];
void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){
if( n.getKind()==MULT ){
- if( n[1].hasAttribute(InstConstantAttribute()) ){
- f = n[1].getAttribute(InstConstantAttribute());
+ if( TermDb::hasInstConstAttr(n[1]) ){
+ f = TermDb::getInstConstAttr(n[1]);
if( n[1].getKind()==INST_CONSTANT ){
d_ceTableaux[x][ n[1] ] = n[0];
}else{
t << n;
}
}else{
- if( n.hasAttribute(InstConstantAttribute()) ){
- f = n.getAttribute(InstConstantAttribute());
+ if( TermDb::hasInstConstAttr(n) ){
+ f = TermDb::getInstConstAttr(n);
if( n.getKind()==INST_CONSTANT ){
d_ceTableaux[x][ n ] = Node::null();
}else{
Node InstStrategyDatatypesValue::getValueFor( Node n ){
//simply get the ground value for n in the current model, if it exists,
// or return an arbitrary ground term otherwise
- if( !n.hasAttribute(InstConstantAttribute()) ){
+ if( !TermDb::hasInstConstAttr(n) ){
return n;
}else{
return n;
}
- /* FIXME
-
- Debug("quant-datatypes-debug") << "get value for " << n << std::endl;
- if( !n.hasAttribute(InstConstantAttribute()) ){
- return n;
- }else{
- Assert( n.getType().isDatatype() );
- //check if in equivalence class with ground term
- Node rep = getRepresentative( n );
- Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl;
- if( !rep.hasAttribute(InstConstantAttribute()) ){
- return rep;
- }else{
- if( !n.getType().isDatatype() ){
- return n.getType().mkGroundTerm();
- }else{
- if( n.getKind()==APPLY_CONSTRUCTOR ){
- std::vector< Node > children;
- children.push_back( n.getOperator() );
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- children.push_back( getValueFor( n[i] ) );
- }
- return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
- }else{
- const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
- TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels;
- //otherwise, use which constructor the inst constant is current chosen to be
- if( labels->find( n )!=labels->end() ){
- TheoryDatatypes::EqList* lbl = (*labels->find( n )).second;
- int tIndex = -1;
- if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){
- Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl;
- tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr());
- }else{
- Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl;
- //must find a possible choice
- vector< bool > possibleCons;
- possibleCons.resize( dt.getNumConstructors(), true );
- for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) {
- Node leqn = (*j);
- possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false;
- }
- for( unsigned int j=0; j<possibleCons.size(); j++ ) {
- if( possibleCons[j] ){
- tIndex = j;
- break;
- }
- }
- }
- Assert( tIndex!=-1 );
- Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() );
- Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl;
- std::vector< Node > children;
- children.push_back( cons );
- for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) {
- Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n );
- if( n.hasAttribute(InstConstantAttribute()) ){
- InstConstantAttribute ica;
- sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) );
- }
- Node snn = getValueFor( sn );
- children.push_back( snn );
- }
- return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
- }else{
- return n.getType().mkGroundTerm();
- }
- }
- }
- }
- }
- */
}
}
+Node QModelBuilder::getCurrentModelValue( FirstOrderModel* fm, Node n, bool partial ) {
+ std::vector< Node > children;
+ if( n.getNumChildren()>0 ){
+ if( n.getKind()!=APPLY_UF && n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ for (unsigned i=0; i<n.getNumChildren(); i++) {
+ Node nc = getCurrentModelValue( fm, n[i] );
+ if (nc.isNull()) {
+ return Node::null();
+ }else{
+ children.push_back( nc );
+ }
+ }
+ if( n.getKind()==APPLY_UF ){
+ return getCurrentUfModelValue( fm, n, children, partial );
+ }else{
+ Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ nn = Rewriter::rewrite( nn );
+ return nn;
+ }
+ }else{
+ if( n.getKind()==VARIABLE ){
+ return getCurrentUfModelValue( fm, n, children, partial );
+ }else{
+ return n;
+ }
+ }
+}
+
+
bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
if( argIndex<(int)n.getNumChildren() ){
Node r;
}
+Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {
+ return n;
+}
void QModelBuilderIG::debugModel( FirstOrderModel* fm ){
//debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
vars.push_back( f[0][j] );
}
- RepSetIterator riter( &(fm->d_rep_set) );
- riter.setQuantifier( d_qe, f );
+ RepSetIterator riter( d_qe, &(fm->d_rep_set) );
+ riter.setQuantifier( f );
while( !riter.isFinished() ){
std::vector< Node > terms;
for( int i=0; i<riter.getNumTerms(); i++ ){
// constant definitions.
bool isConst = true;
std::vector< Node > uf_terms;
- if( n.hasAttribute(InstConstantAttribute()) ){
+ if( TermDb::hasInstConstAttr(n) ){
isConst = false;
if( gn.getKind()==APPLY_UF ){
uf_terms.push_back( gn );
}else if( gn.getKind()==EQUAL ){
isConst = true;
for( int j=0; j<2; j++ ){
- if( n[j].hasAttribute(InstConstantAttribute()) ){
+ if( TermDb::hasInstConstAttr(n[j]) ){
if( n[j].getKind()==APPLY_UF &&
fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){
uf_terms.push_back( gn[j] );
for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){
bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT;
Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i];
- Assert( lit.hasAttribute(InstConstantAttribute()) );
+ Assert( TermDb::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( IFF, lit, !phase ? fm->d_true : fm->d_false );
- d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f );
tr_terms.push_back( eq );
}else if( lit.getKind()==EQUAL ){
//collect trigger terms
for( int j=0; j<2; j++ ){
- if( lit[j].hasAttribute(InstConstantAttribute()) ){
+ if( TermDb::hasInstConstAttr(lit[j]) ){
if( lit[j].getKind()==APPLY_UF ){
tr_terms.push_back( lit[j] );
}else{
//if( !s.isNull() ){
// s = Rewriter::rewrite( s );
//}
- d_qe->getTermDatabase()->setInstantiationConstantAttr( s, f );
Trace("sel-form-debug") << "Selection formula " << f << std::endl;
Trace("sel-form-debug") << " " << s << std::endl;
if( !s.isNull() ){
context::CDO< FirstOrderModel* > d_curr_model;
//quantifiers engine
QuantifiersEngine* d_qe;
+ /** get current model value */
+ virtual Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) = 0;
public:
QModelBuilder( context::Context* c, QuantifiersEngine* qe );
virtual ~QModelBuilder(){}
bool d_considerAxioms;
/** exist instantiation ? */
virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
+ /** get current model value */
+ Node getCurrentModelValue( FirstOrderModel* fm, Node n, bool partial = false );
};
bool d_didInstGen;
/** process build model */
virtual void processBuildModel( TheoryModel* m, bool fullModel );
+ /** get current model value */
+ Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial );
protected:
//reset
virtual void reset( FirstOrderModel* fm ) = 0;
d_relevantLemmas = 0;
d_totalLemmas = 0;
Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
- int e_max = options::fmfFullModelCheck() ? 2 : 1;
+ int e_max = options::fmfFullModelCheck() && options::fmfModelBasedInst() ? 2 : 1;
for( int e=0; e<e_max; e++) {
if (addedLemmas==0) {
for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
}
Debug("inst-fmf-ei") << std::endl;
//create a rep set iterator and iterate over the (relevant) domain of the quantifier
- RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
- if( riter.setQuantifier( d_quantEngine, f ) ){
+ RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
+ if( riter.setQuantifier( f ) ){
Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
d_quantEngine->getModel()->resetEvaluate();
Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
option fmfFreshDistConst --fmf-fresh-dc bool :default false
use fresh distinguished representative when applying Inst-Gen techniques
+option fmfBoundInt --fmf-bound-int bool :default false
+ finite model finding on bounded integer quantification
+
option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
policy for instantiating axioms
for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){
Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl;
if( it->first.getKind()==EQUAL ){
- if( it->first[0].hasAttribute(InstConstantAttribute()) ){
- if( !it->first[1].hasAttribute(InstConstantAttribute()) ){
+ if( quantifiers::TermDb::hasInstConstAttr(it->first[0]) ){
+ if( !quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){
d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];
d_phase_reqs_equality[ it->first[0] ] = it->second;
Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;
}
- }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){
+ }else if( quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){
d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];
d_phase_reqs_equality[ it->first[1] ] = it->second;
Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;
if( in.hasAttribute(NestedQuantAttribute()) ){
setNestedQuantifiers( ret, in.getAttribute(NestedQuantAttribute()) );
}
- if( in.hasAttribute(InstConstantAttribute()) ){
- InstConstantAttribute ica;
- ret.setAttribute(ica,in.getAttribute(InstConstantAttribute()) );
- }
Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
Trace("quantifiers-rewrite") << " to " << std::endl;
Trace("quantifiers-rewrite") << ret << std::endl;
bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){
if( n.getKind()==INST_CONSTANT ){
- Node f = n.getAttribute(InstConstantAttribute());
+ Node f = TermDb::getInstConstAttr(n);
int var = n.getAttribute(InstVarNumAttribute());
range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() );
return false;
}
}
//get the range
- if( n.hasAttribute(InstConstantAttribute()) ){
+ if( TermDb::hasInstConstAttr(n) ){
if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){
range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() );
}else{
//if this is an atomic trigger, consider adding it
//Call the children?
if( inst::Trigger::isAtomicTrigger( n ) ){
- if( !n.hasAttribute(InstConstantAttribute()) ){
+ if( !TermDb::hasInstConstAttr(n) ){
Trace("term-db") << "register term in db " << n << std::endl;
//std::cout << "register trigger term " << n << std::endl;
Node op = n.getOperator();
}
}
}else{
- if( options::efficientEMatching() && !n.hasAttribute(InstConstantAttribute())){
+ if( options::efficientEMatching() && !TermDb::hasInstConstAttr(n)){
//Efficient e-matching must be notified
//The term in triggers are not important here
Debug("term-db") << "New in this branch term " << n << std::endl;
while( !eqc.isFinished() ){
Node en = (*eqc);
computeModelBasisArgAttribute( en );
- if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){
+ if( en.getKind()==APPLY_UF && !TermDb::hasInstConstAttr(en) ){
if( !en.getAttribute(NoMatchAttribute()) ){
Node op = en.getOperator();
if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
//set the var number attribute
InstVarNumAttribute ivna;
ic.setAttribute(ivna,i);
+ InstConstantAttribute ica;
+ ic.setAttribute(ica,f);
+ //also set the no-match attribute
+ NoMatchAttribute nma;
+ ic.setAttribute(nma,true);
}
}
}
-void TermDb::setInstantiationConstantAttr( Node n, Node f ){
- if( !n.hasAttribute(InstConstantAttribute()) ){
- bool setAttr = false;
- if( n.getKind()==INST_CONSTANT ){
- setAttr = true;
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- setInstantiationConstantAttr( n[i], f );
- if( n[i].hasAttribute(InstConstantAttribute()) ){
- setAttr = true;
- }
+
+Node TermDb::getInstConstAttr( Node n ) {
+ if (!n.hasAttribute(InstConstantAttribute()) ){
+ Node f;
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ f = getInstConstAttr(n[i]);
+ if( !f.isNull() ){
+ break;
}
}
- if( setAttr ){
- InstConstantAttribute ica;
- n.setAttribute(ica,f);
+ InstConstantAttribute ica;
+ n.setAttribute(ica,f);
+ if( !f.isNull() ){
//also set the no-match attribute
NoMatchAttribute nma;
n.setAttribute(nma,true);
}
}
+ return n.getAttribute(InstConstantAttribute());
+}
+
+bool TermDb::hasInstConstAttr( Node n ) {
+ return !getInstConstAttr(n).isNull();
}
+bool TermDb::hasBoundVarAttr( Node n ) {
+ if( !n.getAttribute(HasBoundVarComputedAttribute()) ){
+ bool hasBv = false;
+ if( n.getKind()==BOUND_VARIABLE ){
+ hasBv = true;
+ }else{
+ for (unsigned i=0; i<n.getNumChildren(); i++) {
+ if( hasBoundVarAttr(n[i]) ){
+ hasBv = true;
+ break;
+ }
+ }
+ }
+ HasBoundVarAttribute hbva;
+ n.setAttribute(hbva, hasBv);
+ HasBoundVarComputedAttribute hbvca;
+ n.setAttribute(hbvca, true);
+ Trace("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttribute()) << std::endl;
+ }
+ return n.getAttribute(HasBoundVarAttribute());
+}
+
+void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) {
+ if (n.getKind()==BOUND_VARIABLE ){
+ if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){
+ bvs.push_back( n );
+ }
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++) {
+ getBoundVars(n[i], bvs);
+ }
+ }
+}
+
+
/** get the i^th instantiation constant of f */
Node TermDb::getInstantiationConstant( Node f, int i ) const {
std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f );
//otherwise, ensure literal
Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() );
d_ce_lit[ f ] = ceLit;
- setInstantiationConstantAttr( ceLit, f );
}
return d_ce_lit[ f ];
}
Node n2 = n.substitute( vars.begin(), vars.end(),
inst_constants.begin(),
inst_constants.end() );
- setInstantiationConstantAttr( n2, f );
return n2;
}
struct ModelBasisArgAttributeId {};
typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
+struct HasBoundVarAttributeId {};
+typedef expr::Attribute<HasBoundVarAttributeId, bool> HasBoundVarAttribute;
+struct HasBoundVarComputedAttributeId {};
+typedef expr::Attribute<HasBoundVarComputedAttributeId, bool> HasBoundVarComputedAttribute;
class QuantifiersEngine;
Node convertNodeToPattern( Node n, Node f,
const std::vector<Node> & vars,
const std::vector<Node> & nvars);
- /** set instantiation constant attr */
- void setInstantiationConstantAttr( Node n, Node f );
+ static Node getInstConstAttr( Node n );
+ static bool hasInstConstAttr( Node n );
+//for bound variables
+public:
+ //does n have bound variables?
+ static bool hasBoundVarAttr( Node n );
+ //get bound variables in n
+ static void getBoundVars( Node n, std::vector< Node >& bvs);
//for skolem
private:
/** map from universal quantifiers to the list of skolem constants */
void TheoryQuantifiers::preRegisterTerm(TNode n) {
Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
- if( n.getKind()==FORALL && !n.hasAttribute(InstConstantAttribute()) ){
+ if( n.getKind()==FORALL && !TermDb::hasInstConstAttr(n) ){
getQuantifiersEngine()->registerQuantifier( n );
}
}
void TheoryQuantifiers::assertUniversal( Node n ){
Assert( n.getKind()==FORALL );
- if( !n.hasAttribute(InstConstantAttribute()) ){
+ if( !TermDb::hasInstConstAttr(n) ){
getQuantifiersEngine()->registerQuantifier( n );
getQuantifiersEngine()->assertNode( n );
}
void TheoryQuantifiers::assertExistential( Node n ){
Assert( n.getKind()== NOT && n[0].getKind()==FORALL );
- if( !n[0].hasAttribute(InstConstantAttribute()) ){
+ if( !TermDb::hasInstConstAttr(n[0]) ){
if( d_skolemized.find( n )==d_skolemized.end() ){
Node body = getQuantifiersEngine()->getTermDatabase()->getSkolemizedBody( n[0] );
NodeBuilder<> nb(kind::OR);
qe->getTermDatabase()->computeVarContains( temp[i] );
for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){
Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j];
- if( v.getAttribute(InstConstantAttribute())==f ){
+ if( quantifiers::TermDb::getInstConstAttr(v)==f ){
if( vars.find( v )==vars.end() ){
varCount++;
vars[ v ] = true;
}
bool Trigger::isUsable( Node n, Node f ){
- if( n.getAttribute(InstConstantAttribute())==f ){
+ if( quantifiers::TermDb::getInstConstAttr(n)==f ){
if( isAtomicTrigger( n ) ){
for( int i=0; i<(int)n.getNumChildren(); i++ ){
if( !isUsable( n[i], f ) ){
int vti = veq[0]==it->first ? 1 : 0;
if( isUsableTrigger(veq[vti], f) && !nodeContainsVar( veq[vti], veq[vti==0 ? 1 : 0]) ){
rtr = veq;
- InstConstantAttribute ica;
- rtr.setAttribute(ica,veq[vti].getAttribute(InstConstantAttribute()) );
}
}
}
Trace("relational-trigger") << " polarity : " << pol << std::endl;
}
Node rtr2 = (hasPol && pol) ? rtr.negate() : rtr;
- InstConstantAttribute ica;
- rtr2.setAttribute(ica,rtr.getAttribute(InstConstantAttribute()) );
return rtr2;
}
}
}
- bool usable = n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f );
+ bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f );
Trace("usable") << n << " usable : " << usable << std::endl;
if( usable ){
return n;
bool Trigger::isSimpleTrigger( Node n ){
if( isAtomicTrigger( n ) ){
for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){
+ if( n[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(n[i]) ){
return false;
}
}
Assert( coeffs.empty() );
NodeBuilder<> t(kind::PLUS);
for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( n[i].hasAttribute(InstConstantAttribute()) ){
+ if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){
if( n[i].getKind()==INST_CONSTANT ){
- if( n[i].getAttribute(InstConstantAttribute())==f ){
+ if( quantifiers::TermDb::getInstConstAttr(n[i])==f ){
coeffs[ n[i] ] = Node::null();
}else{
coeffs.clear();
}
return true;
}else if( n.getKind()==MULT ){
- if( n[0].getKind()==INST_CONSTANT && n[0].getAttribute(InstConstantAttribute())==f ){
- if( !n[1].hasAttribute(InstConstantAttribute()) ){
+ if( n[0].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[0])==f ){
+ if( !quantifiers::TermDb::hasInstConstAttr(n[1]) ){
coeffs[ n[0] ] = n[1];
return true;
}
- }else if( n[1].getKind()==INST_CONSTANT && n[1].getAttribute(InstConstantAttribute())==f ){
- if( !n[0].hasAttribute(InstConstantAttribute()) ){
+ }else if( n[1].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[1])==f ){
+ if( !quantifiers::TermDb::hasInstConstAttr(n[0]) ){
coeffs[ n[1] ] = n[0];
return true;
}
if( options::finiteModelFind() ){
d_model_engine = new quantifiers::ModelEngine( c, this );
d_modules.push_back( d_model_engine );
-
- d_bint = new quantifiers::BoundedIntegers( c, this );
- d_modules.push_back( d_bint );
+ if( options::fmfBoundInt() ){
+ d_bint = new quantifiers::BoundedIntegers( c, this );
+ d_modules.push_back( d_bint );
+ }else{
+ d_bint = NULL;
+ }
}else{
d_model_engine = NULL;
d_bint = NULL;
bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
Assert( f.getKind()==FORALL );
- Assert( !f.hasAttribute(InstConstantAttribute()) );
Assert( vars.size()==terms.size() );
Node body = getInstantiation( f, vars, terms );
//make the lemma
Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
uint64_t maxInstLevel = 0;
for( int i=0; i<(int)terms.size(); i++ ){
- if( terms[i].hasAttribute(InstConstantAttribute()) ){
+ if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){
Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
for( int i=0; i<(int)terms.size(); i++ ){
Debug("inst") << " " << terms[i] << std::endl;
}
bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){
- //Assert( !n1.hasAttribute(InstConstantAttribute()) );
- //Assert( !n2.hasAttribute(InstConstantAttribute()) );
//Assert( !areEqual( n1, n2 ) );
//Assert( !areDisequal( n1, n2 ) );
Kind knd = n1.getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){
bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] );
nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
- d_term_db->setInstantiationConstantAttr( nodes[i], f );
nodeChanged = true;
}
//else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
}
-RepSetIterator::RepSetIterator( RepSet* rs ) : d_rep_set( rs ){
+RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), d_rep_set( rs ){
d_incomplete = false;
-
}
int RepSetIterator::domainSize( int i ) {
}
}
-bool RepSetIterator::setQuantifier( QuantifiersEngine * qe, Node f ){
+bool RepSetIterator::setQuantifier( Node f ){
+ Trace("rsi") << "Make rsi for " << f << std::endl;
Assert( d_types.empty() );
//store indicies
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
d_types.push_back( f[0][i].getType() );
}
- return initialize(qe, f);
+ d_owner = f;
+ return initialize();
}
-bool RepSetIterator::setFunctionDomain( QuantifiersEngine * qe, Node op ){
+bool RepSetIterator::setFunctionDomain( Node op ){
+ Trace("rsi") << "Make rsi for " << op << std::endl;
Assert( d_types.empty() );
TypeNode tn = op.getType();
for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
d_types.push_back( tn[i] );
}
- return initialize(qe, Node::null());
+ d_owner = op;
+ return initialize();
}
-bool RepSetIterator::initialize(QuantifiersEngine * qe, Node f){
+bool RepSetIterator::initialize(){
for( size_t i=0; i<d_types.size(); i++ ){
d_index.push_back( 0 );
//store default index order
}
}else if( tn.isInteger() ){
//check if it is bound
- if( !f.isNull() && qe && qe->getBoundedIntegers() ){
- Node l = qe->getBoundedIntegers()->getLowerBoundValue( f, f[0][i] );
- Node u = qe->getBoundedIntegers()->getUpperBoundValue( f, f[0][i] );
- if( !l.isNull() && !u.isNull() ){
- Trace("bound-int-reps") << "Can limit bounds of " << f[0][i] << " to " << l << "..." << u << std::endl;
- Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
- Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
- if( ra==NodeManager::currentNM()->mkConst(true) ){
- long rr = range.getConst<Rational>().getNumerator().getLong()+1;
- if (rr<0) {
- Trace("bound-int-reps") << "Empty bound range." << std::endl;
- //empty
- d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
- }else{
- Trace("bound-int-reps") << "Actual bound range is " << rr << std::endl;
- d_lower_bounds[i] = l;
- d_domain[i].push_back( (int)rr );
- d_enum_type.push_back( ENUM_RANGE );
- }
- isSet = true;
- }else{
- Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big." << std::endl;
- d_incomplete = true;
- }
+ if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
+ if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][i] ) ){
+ Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded integer." << std::endl;
+ d_enum_type.push_back( ENUM_RANGE );
+ isSet = true;
}else{
Trace("fmf-incomplete") << "Incomplete because of integer quantification, no bounds found." << std::endl;
d_incomplete = true;
}
}
}
+ //must set a variable index order
+ if (d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers()) {
+ Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
+ std::vector< int > varOrder;
+ for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars(d_owner); i++ ){
+ varOrder.push_back(d_qe->getBoundedIntegers()->getBoundVarNum(d_owner,i));
+ }
+ for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) {
+ if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) {
+ varOrder.push_back(i);
+ }
+ }
+ Trace("bound-int-rsi") << "Variable order : ";
+ for( unsigned i=0; i<varOrder.size(); i++) {
+ Trace("bound-int-rsi") << varOrder[i] << " ";
+ }
+ Trace("bound-int-rsi") << std::endl;
+ std::vector< int > indexOrder;
+ indexOrder.resize(varOrder.size());
+ for( unsigned i=0; i<varOrder.size(); i++){
+ indexOrder[varOrder[i]] = i;
+ }
+ Trace("bound-int-rsi") << "Will use index order : ";
+ for( unsigned i=0; i<indexOrder.size(); i++) {
+ Trace("bound-int-rsi") << indexOrder[i] << " ";
+ }
+ Trace("bound-int-rsi") << std::endl;
+ setIndexOrder(indexOrder);
+ }
+ for (unsigned i=0; i<d_index.size(); i++) {
+ if (!resetIndex(i, true)){
+ break;
+ }
+ }
return true;
}
}
}
*/
+bool RepSetIterator::resetIndex( int i, bool initial ) {
+ d_index[i] = 0;
+ int ii = d_index_order[i];
+ Trace("bound-int-rsi") << "Reset " << i << " " << ii << " " << initial << std::endl;
+ //determine the current range
+ if( d_enum_type[ii]==ENUM_RANGE ){
+ if( initial || !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ){
+ Trace("bound-int-rsi") << "Getting range of " << d_owner[0][ii] << std::endl;
+ Node l, u;
+ d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u );
+ if( l.isNull() || u.isNull() ){
+ //failed, abort the iterator
+ d_index.clear();
+ return false;
+ }else{
+ Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][ii] << " to " << l << "..." << u << std::endl;
+ Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
+ Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
+ d_domain[ii].clear();
+ d_lower_bounds[ii] = l;
+ if( ra==NodeManager::currentNM()->mkConst(true) ){
+ long rr = range.getConst<Rational>().getNumerator().getLong()+1;
+ Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl;
+ d_domain[ii].push_back( (int)rr );
+ }else{
+ Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner[0][ii] << "." << std::endl;
+ d_incomplete = true;
+ d_domain[ii].push_back( 0 );
+ }
+ }
+ }else{
+ Trace("bound-int-rsi") << d_owner[0][ii] << " has ground range, skip." << std::endl;
+ }
+ }
+ return true;
+}
+
void RepSetIterator::increment2( int counter ){
Assert( !isFinished() );
#ifdef DISABLE_EVAL_SKIP_MULTIPLE
counter = (int)d_index.size()-1;
#endif
//increment d_index
- while( counter>=0 && d_index[counter]==(int)(domainSize(counter)-1) ){
+ Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
+ while( counter>=0 && d_index[counter]>=(int)(domainSize(counter)-1) ){
counter--;
+ if( counter>=0){
+ Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
+ }
}
if( counter==-1 ){
d_index.clear();
}else{
+ d_index[counter]++;
for( int i=(int)d_index.size()-1; i>counter; i-- ){
- d_index[i] = 0;
+ if (!resetIndex(i)){
+ break;
+ }
}
- d_index[counter]++;
}
}
Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() );
return d_rep_set->d_type_reps[tn][d_domain[index][d_index[index]]];
}else{
+ Trace("rsi-debug") << index << " " << d_lower_bounds[index] << " " << d_index[index] << std::endl;
Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[index],
NodeManager::currentNM()->mkConst( Rational(d_index[index]) ) );
t = Rewriter::rewrite( t );
ENUM_DOMAIN_ELEMENTS,
ENUM_RANGE,
};
-
+ QuantifiersEngine * d_qe;
//initialize function
- bool initialize(QuantifiersEngine * qe, Node f);
+ bool initialize();
//enumeration type?
std::vector< int > d_enum_type;
//for enum ranges
std::map< int, Node > d_lower_bounds;
//domain size
int domainSize( int i );
+ //node this is rep set iterator is for
+ Node d_owner;
+ //reset index
+ bool resetIndex( int i, bool initial = false );
public:
- RepSetIterator( RepSet* rs );
+ RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
~RepSetIterator(){}
//set that this iterator will be iterating over instantiations for a quantifier
- bool setQuantifier( QuantifiersEngine * qe, Node f );
+ bool setQuantifier( Node f );
//set that this iterator will be iterating over the domain of a function
- bool setFunctionDomain( QuantifiersEngine * qe, Node op );
+ bool setFunctionDomain( Node op );
public:
//pointer to model
RepSet* d_rep_set;
/* The order of the matching is:
reset arg1, nextMatch arg1, reset arg2, nextMatch arg2, ... */
ApplyMatcher::ApplyMatcher( Node pat, QuantifiersEngine* qe): d_pattern(pat){
- // Assert( pat.hasAttribute(InstConstantAttribute()) );
//set-up d_variables, d_constants, d_childrens
for( size_t i=0; i< d_pattern.getNumChildren(); ++i ){
//EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType());
EqualityQuery* q = qe->getEqualityQuery();
Assert( q != NULL );
- if( d_pattern[i].hasAttribute(InstConstantAttribute()) ){
+ if( quantifiers::TermDb::hasInstConstAttr(d_pattern[i]) ){
if( d_pattern[i].getKind()==INST_CONSTANT ){
//It's a variable
d_variables.push_back(make_triple((TNode)d_pattern[i],i,q));
//if t is null
Assert( !t.isNull() );
- Assert( !t.hasAttribute(InstConstantAttribute()) );
+ Assert( !quantifiers::TermDb::hasInstConstAttr(t) );
Assert( t.getKind()==d_pattern.getKind() );
Assert( (t.getKind()!=APPLY_UF && t.getKind()!=APPLY_CONSTRUCTOR)
|| t.getOperator()==d_pattern.getOperator() );
size_t numFreeVar(TNode t){
size_t n = 0;
for( size_t i=0, size =t.getNumChildren(); i < size; ++i ){
- if( t[i].hasAttribute(InstConstantAttribute()) ){
+ if( quantifiers::TermDb::hasInstConstAttr(t[i]) ){
if( t[i].getKind()==INST_CONSTANT ){
//variable
++n;
/** TODO: something simpler to see if the pattern is a good
arithmetic pattern */
std::map< Node, Node > d_arith_coeffs;
- if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){
+ if( !Trigger::getPatternArithmetic( quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) ){
Message() << "(?) Unknown matching pattern is " << pat << std::endl;
Unimplemented("pattern not implemented");
return new DumbMatcher();
PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){
Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;
- Assert( pat.hasAttribute(InstConstantAttribute()) );
+ Assert( quantifiers::TermDb::hasInstConstAttr(pat) );
if( pat.getKind()==kind::NOT && pat[0].getKind() == kind::EQUAL){
/* Difference */
return new UfDeqMatcher(pat, qe);
} else if (pat.getKind() == kind::EQUAL){
- if( !pat[0].hasAttribute(InstConstantAttribute() )){
- Assert(pat[1].hasAttribute(InstConstantAttribute()));
+ if( !quantifiers::TermDb::hasInstConstAttr(pat[0])){
+ Assert(quantifiers::TermDb::hasInstConstAttr(pat[1]));
return new UfCstEqMatcher(pat[1], pat[0], qe);
- }else if( !pat[1].hasAttribute(InstConstantAttribute() )){
- Assert(pat[0].hasAttribute(InstConstantAttribute()));
+ }else if( !quantifiers::TermDb::hasInstConstAttr(pat[1] )){
+ Assert(quantifiers::TermDb::hasInstConstAttr(pat[0]));
return new UfCstEqMatcher(pat[0], pat[1], qe);
}else{
std::vector< Node > pats(pat.begin(),pat.end());
/** TODO: something simpler to see if the pattern is a good
arithmetic pattern */
std::map< Node, Node > d_arith_coeffs;
- if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){
+ if( !Trigger::getPatternArithmetic( quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) ){
Debug("inst-match-gen") << "(?) Unknown matching pattern is " << pat << std::endl;
Message() << "(?) Unknown matching pattern is " << pat << std::endl;
return new DumbPatMatcher();
ArithMatcher::ArithMatcher(Node pat, QuantifiersEngine* qe): d_pattern(pat){
- if(Trigger::getPatternArithmetic(pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) )
+ if(Trigger::getPatternArithmetic(quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) )
{
Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_pattern << std::endl;
Assert(false);
/** legal candidate */
static inline bool isLegalCandidate( TNode n ){
return !n.getAttribute(NoMatchAttribute()) &&
- ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute())) &&
+ ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n)) &&
( !options::efficientEMatching() || n.hasAttribute(AvailableInTermDb()) );
}
int Trigger::addInstantiations( InstMatch& baseMatch ){
int addedLemmas = d_mg->addInstantiations( baseMatch,
- d_nodes[0].getAttribute(InstConstantAttribute()),
+ quantifiers::TermDb::getInstConstAttr(d_nodes[0]),
d_quantEngine);
if( addedLemmas>0 ){
Debug("inst-trigger") << "Added " << addedLemmas << " lemmas, trigger was ";
qe->getTermDatabase()->computeVarContains( temp[i] );
for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){
Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j];
- if( v.getAttribute(InstConstantAttribute())==f ){
+ if( quantifiers::TermDb::getInstConstAttr(v)==f ){
if( vars.find( v )==vars.end() ){
vars[ v ] = true;
foundVar = true;
}
bool Trigger::isUsable( Node n, Node f ){
- if( n.getAttribute(InstConstantAttribute())==f ){
+ if( quantifiers::TermDb::getInstConstAttr(n)==f ){
if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){
std::map< Node, Node > coeffs;
return getPatternArithmetic( f, n, coeffs );
bool Trigger::isSimpleTrigger( Node n ){
if( isAtomicTrigger( n ) ){
for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){
+ if( n[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(n[i]) ){
return false;
}
}
Assert( coeffs.empty() );
NodeBuilder<> t(kind::PLUS);
for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( n[i].hasAttribute(InstConstantAttribute()) ){
+ if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){
if( n[i].getKind()==INST_CONSTANT ){
- if( n[i].getAttribute(InstConstantAttribute())==f ){
+ if( quantifiers::TermDb::getInstConstAttr(n[i])==f ){
coeffs[ n[i] ] = Node::null();
}else{
coeffs.clear();
}
return true;
}else if( n.getKind()==MULT ){
- if( n[0].getKind()==INST_CONSTANT && n[0].getAttribute(InstConstantAttribute())==f ){
- Assert( !n[1].hasAttribute(InstConstantAttribute()) );
+ if( n[0].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[0])==f ){
+ Assert( !quantifiers::TermDb::hasInstConstAttr(n[1]) );
coeffs[ n[0] ] = n[1];
return true;
- }else if( n[1].getKind()==INST_CONSTANT && n[1].getAttribute(InstConstantAttribute())==f ){
- Assert( !n[0].hasAttribute(InstConstantAttribute()) );
+ }else if( n[1].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[1])==f ){
+ Assert( !quantifiers::TermDb::hasInstConstAttr(n[0]) );
coeffs[ n[1] ] = n[0];
return true;
}
public:
/** is usable trigger */
static inline bool isUsableTrigger( TNode n, TNode f ){
- //return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF;
- return n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f );
+ return quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f );
}
static inline bool isAtomicTrigger( TNode n ){
return
rewriter::Subst & vars);
//create inst variable
- std::vector<Node> createInstVariable( std::vector<Node> & vars );
+ std::vector<Node> createInstVariable( Node r, std::vector<Node> & vars );
/** statistics class */
class Statistics {
vars.push_back(*v);
};
/* Instantiation version */
- std::vector<Node> inst_constants = createInstVariable(vars);
+ std::vector<Node> inst_constants = createInstVariable(r,vars);
/* Body/Remove_term/Guards/Triggers */
Node body = r[2][1];
TNode new_terms = r[2][1];
}
-std::vector<Node> TheoryRewriteRules::createInstVariable( std::vector<Node> & vars ){
+std::vector<Node> TheoryRewriteRules::createInstVariable( Node r, std::vector<Node> & vars ){
std::vector<Node> inst_constant;
inst_constant.reserve(vars.size());
for( std::vector<Node>::const_iterator v = vars.begin();
//make instantiation constants
Node ic = NodeManager::currentNM()->mkInstConstant( (*v).getType() );
inst_constant.push_back( ic );
+ InstConstantAttribute ica;
+ ic.setAttribute(ica,r);
+ //also set the no-match attribute
+ NoMatchAttribute nma;
+ ic.setAttribute(nma,true);
};
return inst_constant;
}
projects / cvc5.git / commitdiff