std::vector< Node > mbp_vts_coeff[2][2];
std::vector< Node > mbp_lit[2];
//std::vector< MbpBounds > mbp_bounds[2];
- unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
- for( unsigned r=0; r<rmax; r++ ){
- TheoryId tid = r==0 ? Theory::theoryOf( pv ) : Theory::theoryOf( pv.getType() );
+ //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
+ for( unsigned r=0; r<2; r++ ){
+ TheoryId tid = r==0 ? Theory::theoryOf( pvtn ) : THEORY_UF;
Trace("cbqi-inst-debug2") << " look at assertions of " << tid << std::endl;
std::map< TheoryId, std::vector< Node > >::iterator ita = d_curr_asserts.find( tid );
if( ita!=d_curr_asserts.end() ){
Trace("cbqi-inst-debug2") << " look at " << lit << std::endl;
Node atom = lit.getKind()==NOT ? lit[0] : lit;
bool pol = lit.getKind()!=NOT;
- if( tid==THEORY_ARITH ){
+ if( pvtn.isReal() ){
//arithmetic inequalities and disequalities
if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){
Assert( atom[0].getType().isInteger() || atom[0].getType().isReal() );
//[4] resort to using value in model
// do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype
- if( effort>0 || pvtn.isBoolean() || !curr_var.empty() ){
+ if( ( effort>0 || pvtn.isBoolean() || !curr_var.empty() ) && !pvtn.isSort() ){
Node mv = getModelValue( pv );
Node pv_coeff_m;
Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
}
Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) {
- /*
- if( e.getType().isInteger() && !t.getType().isInteger() ){
- //TODO : round up/down this bound?
- return Node::null();
- }
- */
Node val = t;
Trace("cbqi-bound2") << "Value : " << val << std::endl;
+ Assert( !e.getType().isInteger() || t.getType().isInteger() );
+ Assert( !e.getType().isInteger() || mt.getType().isInteger() );
//add rho value
//get the value of c*e
Node ceValue = me;
Node rho;
//if( !mt.getType().isInteger() ){
//round up/down
- //mt = NodeManager::currentNM()->mkNode(
+ //mt = NodeManager::currentNM()->mkNode(
//}
if( isLower ){
rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt );
//for each variable
std::vector< TheoryId > tids;
+ tids.push_back(THEORY_UF);
for( unsigned i=0; i<d_vars.size(); i++ ){
Node pv = d_vars[i];
TypeNode pvtn = pv.getType();
d_var_order_index.clear();
}
}
-
- //remove ITEs
+
+ //remove ITEs
IteSkolemMap iteSkolemMap;
d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
Assert( d_aux_vars.empty() );
}
}
}
-
+
ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() );
if( ires!=0 ){
Node realPart;
Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
Trace("cbqi-inst-debug") << " real part : " << realPart << std::endl;
if( ires!=0 ){
- val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires==-1 ? PLUS : MINUS,
+ val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires==-1 ? PLUS : MINUS,
NodeManager::currentNM()->mkNode( ires==-1 ? MINUS : PLUS, val, realPart ),
NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) );
Trace("cbqi-inst-debug") << "result : " << val << std::endl;
vts_coeff_inf = vts_coeff[0];
vts_coeff_delta = vts_coeff[1];
}
-
+
return ires;
}
#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ){
-
+
}
bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) {
for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
- if( d_quantEngine->getOwner( q )==this && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+ if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
return QuantifiersEngine::QEFFORT_STANDARD;
}
}
for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
//it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
- if( d_quantEngine->getOwner( q )==this ){
+ if( doCbqi( q ) ){
if( !hasAddedCbqiLemma( q ) ){
d_added_cbqi_lemma.insert( q );
Trace("cbqi") << "Do cbqi for " << q << std::endl;
Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
registerCounterexampleLemma( q, lem );
}
- //set inactive the quantified formulas whose CE literals are asserted false
+ //set inactive the quantified formulas whose CE literals are asserted false
}else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
- if( d_quantEngine->getOwner( q )==this && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+ if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
process( q, e, ee );
}
}
void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
- //take ownership of the quantified formula
- d_quantEngine->setOwner( q, this );
+ if( !options::cbqiAll() && !options::cbqiSplx() ){
+ //take full ownership of the quantified formula
+ d_quantEngine->setOwner( q, this );
+ }
}
}
void InstStrategyCbqi::registerQuantifier( Node q ) {
-
+
}
void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
using namespace CVC4::theory::inst;
InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) :
-QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL){
-
-}
-
-InstantiationEngine::~InstantiationEngine() {
- delete d_i_ag;
- delete d_isup;
-}
-
-void InstantiationEngine::finishInit(){
+QuantifiersModule( qe ){
if( options::eMatching() ){
//these are the instantiation strategies for E-matching
//user-provided patterns
//auto-generated patterns
d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine );
d_instStrategies.push_back( d_i_ag );
+ }else{
+ d_isup = NULL;
+ d_i_ag = NULL;
}
}
+InstantiationEngine::~InstantiationEngine() {
+ delete d_i_ag;
+ delete d_isup;
+}
+
+
void InstantiationEngine::presolve() {
for( unsigned i=0; i<d_instStrategies.size(); ++i ){
d_instStrategies[i]->presolve();
public:
InstantiationEngine( QuantifiersEngine* qe );
~InstantiationEngine();
- /** initialize */
- void finishInit();
void presolve();
bool needsCheck( Theory::Effort e );
void reset_round( Theory::Effort e );
#ite lift mode for quantified formulas
option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToIteLiftQuantMode :handler-include "theory/quantifiers/options_handlers.h"
ite lifting mode for quantified formulas
-option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true
- split variables occurring as conditions of ITE in quantifiers
+option condVarSplitQuant --cond-var-split-quant bool :default true
+ split quantified formulas that lead to variable eliminations
+option condVarSplitQuantAgg --cond-var-split-agg-quant bool :default false
+ aggressive split quantified formulas that lead to variable eliminations
option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false
split ites with dt testers as conditions
# Whether to CNF quantifier bodies
}
if( !d_unassigned.empty() && ( success || doContinue ) ){
- Trace("qcf-check") << "Assign to unassigned..." << std::endl;
+ Trace("qcf-check") << "Assign to unassigned (" << d_unassigned.size() << ")..." << std::endl;
do {
if( doFail ){
Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;
}
}
}while( success && isMatchSpurious( p ) );
+ Trace("qcf-check") << "done assigning." << std::endl;
}
if( success ){
for( unsigned i=0; i<d_unassigned.size(); i++ ){
itt->second.push_back( r );
}
}else{
- d_eqcs[rtn].push_back( r );
+ if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){
+ d_eqcs[rtn].push_back( r );
+ }
}
}
++eqcs_i;
}
}
-Node QuantifiersRewriter::computeProcessIte( Node body ){
- if( body.getKind()==ITE ){
- if( options::iteDtTesterSplitQuant() ){
- Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
- std::map< Node, Node > pcons;
- std::map< Node, std::map< int, Node > > ncons;
- std::vector< Node > conj;
- computeDtTesterIteSplit( body, pcons, ncons, conj );
- Assert( !conj.empty() );
- if( conj.size()>1 ){
- Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl;
- for( unsigned i=0; i<conj.size(); i++ ){
- Trace("quantifiers-rewrite-ite") << " " << conj[i] << std::endl;
+
+bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){
+ if( n.getKind()==NOT ){
+ return isConditionalVariableElim( n[0], -pol );
+ }else if( ( n.getKind()==AND && pol>=0 ) || ( n.getKind()==OR && pol<=0 ) ){
+ pol = n.getKind()==AND ? 1 : -1;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( isConditionalVariableElim( n[i], pol ) ){
+ return true;
+ }
+ }
+ }else if( n.getKind()==EQUAL ){
+ for( unsigned i=0; i<2; i++ ){
+ if( n[i].getKind()==BOUND_VARIABLE ){
+ if( !TermDb::containsTerm( n[1-i], n[i] ) ){
+ return true;
}
- return NodeManager::currentNM()->mkNode( AND, conj );
}
}
- if( options::iteCondVarSplitQuant() ){
- Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
+ }else if( n.getKind()==BOUND_VARIABLE ){
+ return true;
+ }
+ return false;
+}
+
+Node QuantifiersRewriter::computeProcessIte( Node body, Node ipl ){
+ if( options::iteDtTesterSplitQuant() && body.getKind()==ITE ){
+ Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
+ std::map< Node, Node > pcons;
+ std::map< Node, std::map< int, Node > > ncons;
+ std::vector< Node > conj;
+ computeDtTesterIteSplit( body, pcons, ncons, conj );
+ Assert( !conj.empty() );
+ if( conj.size()>1 ){
+ Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl;
+ for( unsigned i=0; i<conj.size(); i++ ){
+ Trace("quantifiers-rewrite-ite") << " " << conj[i] << std::endl;
+ }
+ return NodeManager::currentNM()->mkNode( AND, conj );
+ }
+ }
+ if( options::condVarSplitQuant() ){
+ if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() && !TermDb::isFunDefAnnotation( ipl ) ) ){
+ Trace("quantifiers-rewrite-debug") << "Conditional var elim split " << body << "?" << std::endl;
bool do_split = false;
- for( unsigned r=0; r<2; r++ ){
- //check if there is a variable elimination
- Node b = r==0 ? body[0] : body[0].negate();
- QuantPhaseReq qpr( b );
- Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl;
- for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
- Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl;
- if( it->second ){
- if( it->first.getKind()==EQUAL ){
- for( unsigned i=0; i<2; i++ ){
- if( it->first[i].getKind()==BOUND_VARIABLE ){
- unsigned j = i==0 ? 1 : 0;
- if( !TermDb::containsTerm( it->first[j], it->first[i] ) ){
- do_split = true;
- break;
- }
- }
+ unsigned index_max = body.getKind()==ITE ? 0 : 1;
+ for( unsigned index=0; index<=index_max; index++ ){
+ if( isConditionalVariableElim( body[index] ) ){
+ do_split = true;
+ break;
+ }
+ }
+ if( do_split ){
+ Node pos;
+ Node neg;
+ if( body.getKind()==ITE ){
+ pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
+ neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
+ }else{
+ pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
+ neg = NodeManager::currentNM()->mkNode( OR, body[0], body[1].negate() );
+ }
+ Trace("quantifiers-rewrite-debug") << "*** Split (conditional variable eq) " << body << " into : " << std::endl;
+ Trace("quantifiers-rewrite-debug") << " " << pos << std::endl;
+ Trace("quantifiers-rewrite-debug") << " " << neg << std::endl;
+ return NodeManager::currentNM()->mkNode( AND, pos, neg );
+ }
+ }else if( body.getKind()==OR && options::condVarSplitQuantAgg() ){
+ std::vector< Node > bchildren;
+ std::vector< Node > nchildren;
+ for( unsigned i=0; i<body.getNumChildren(); i++ ){
+ bool split = false;
+ if( nchildren.empty() ){
+ if( body[i].getKind()==AND ){
+ std::vector< Node > children;
+ for( unsigned j=0; j<body[i].getNumChildren(); j++ ){
+ if( ( body[i][j].getKind()==NOT && body[i][j][0].getKind()==EQUAL && isConditionalVariableElim( body[i][j][0] ) ) ||
+ body[i][j].getKind()==BOUND_VARIABLE ){
+ nchildren.push_back( body[i][j] );
+ }else{
+ children.push_back( body[i][j] );
}
}
- }
- if( do_split ){
- break;
+ if( !nchildren.empty() ){
+ if( !children.empty() ){
+ nchildren.push_back( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children ) );
+ }
+ split = true;
+ }
}
}
- if( do_split ){
- //bool cpol = (r==1);
- Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
- //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- //pos = Rewriter::rewrite( pos );
- Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
- Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl;
- Trace("quantifiers-rewrite-ite") << " " << pos << std::endl;
- Trace("quantifiers-rewrite-ite") << " " << neg << std::endl;
- return NodeManager::currentNM()->mkNode( AND, pos, neg );
+ if( !split ){
+ bchildren.push_back( body[i] );
}
}
+ if( !nchildren.empty() ){
+ Trace("quantifiers-rewrite-debug") << "*** Split (conditional variable eq) " << body << " into : " << std::endl;
+ for( unsigned i=0; i<nchildren.size(); i++ ){
+ bchildren.push_back( nchildren[i] );
+ nchildren[i] = NodeManager::currentNM()->mkNode( OR, bchildren );
+ Trace("quantifiers-rewrite-debug") << " " << nchildren[i] << std::endl;
+ bchildren.pop_back();
+ }
+ return NodeManager::currentNM()->mkNode( AND, nchildren );
+ }
}
}
return body;
break;
}
}
- }
- else if( it->first.getKind()==APPLY_TESTER ){
+ }else if( it->first.getKind()==APPLY_TESTER ){
if( options::dtVarExpandQuant() && it->second && it->first[0].getKind()==BOUND_VARIABLE ){
- Trace("dt-var-expand") << "Expand datatype variable based on : " << it->first << std::endl;
+ Trace("var-elim-dt") << "Expand datatype variable based on : " << it->first << std::endl;
std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[0] );
if( ita!=args.end() ){
vars.push_back( it->first[0] );
newVars.push_back( v );
}
subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) );
- Trace("dt-var-expand") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl;
+ Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl;
args.erase( ita );
args.insert( args.end(), newVars.begin(), newVars.end() );
}
}
+ }else if( it->first.getKind()==BOUND_VARIABLE ){
+ if( options::varElimQuant() ){
+ std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first );
+ if( ita!=args.end() ){
+ Trace("var-elim-bool") << "Variable eliminate : " << it->first << " in " << body << std::endl;
+ vars.push_back( it->first );
+ subs.push_back( NodeManager::currentNM()->mkConst( it->second ) );
+ args.erase( ita );
+ }
+ }
}
}
if( !vars.empty() ){
return true;
//return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
}else if( computeOption==COMPUTE_PROCESS_ITE ){
- return options::iteDtTesterSplitQuant() || options::iteCondVarSplitQuant();
+ return options::iteDtTesterSplitQuant() || options::condVarSplitQuant();
}else if( computeOption==COMPUTE_PRENEX ){
return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
}else if( computeOption==COMPUTE_VAR_ELIMINATION ){
n = NodeManager::currentNM()->mkNode( OR, new_conds );
}
}else if( computeOption==COMPUTE_PROCESS_ITE ){
- n = computeProcessIte( n );
+ n = computeProcessIte( n, ipl );
}else if( computeOption==COMPUTE_PRENEX ){
n = computePrenex( n, args, true );
}else if( computeOption==COMPUTE_VAR_ELIMINATION ){
static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl );
static Node computeClause( Node n );
static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
+ static bool isConditionalVariableElim( Node n, int pol=0 );
private:
static Node computeElimSymbols( Node body );
static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl );
static Node computeProcessTerms( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
std::map< Node, Node >& cache, std::map< Node, Node >& icache,
std::vector< Node >& new_vars, std::vector< Node >& new_conds );
- static Node computeProcessIte( Node body );
+ static Node computeProcessIte( Node body, Node ipl );
static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
COMPUTE_AGGRESSIVE_MINISCOPING,
COMPUTE_NNF,
COMPUTE_PROCESS_TERMS,
- COMPUTE_PROCESS_ITE,
COMPUTE_PRENEX,
COMPUTE_VAR_ELIMINATION,
+ COMPUTE_PROCESS_ITE,
//COMPUTE_FLATTEN_ARGS_UF,
//COMPUTE_CNF,
COMPUTE_LAST
return !getFunDefHead( q ).isNull();
}
+bool TermDb::isFunDefAnnotation( Node ipl ) {
+ if( !ipl.isNull() ){
+ for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
+ if( ipl[i].getKind()==INST_ATTRIBUTE ){
+ if( ipl[i][0].getAttribute(FunDefAttribute()) ){
+ return true;
+ }
+ }
+ }
+ }
+ return false;
+}
+
Node TermDb::getFunDefHead( Node q ) {
//&& ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF &&
if( q.getKind()==FORALL && q.getNumChildren()==3 ){
+
for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
if( q[2][i].getKind()==INST_ATTRIBUTE ){
if( q[2][i][0].getAttribute(FunDefAttribute()) ){
/** constants */
Node d_zero;
Node d_one;
-
+
/** map from operators to ground terms for that operator */
std::map< Node, std::vector< Node > > d_op_map;
/** map from type nodes to terms of that type */
std::map< TypeNode, std::vector< Node > > d_type_map;
-
-
+
+
/** count number of non-redundant ground terms per operator */
std::map< Node, int > d_op_nonred_count;
/**mapping from UF terms to representatives of their arguments */
std::map< Node, bool > d_has_map;
/** map from reps to a term in eqc in d_has_map */
std::map< Node, Node > d_term_elig_eqc;
-
+
public:
/** ground terms for operator */
unsigned getNumGroundTerms( Node f );
Node getEligibleTermInEqc( TNode r );
/** is inst closure */
bool isInstClosure( Node r );
-
+
//for model basis
private:
//map from types to model basis terms
bool isClosedEnumerableType( TypeNode tn );
// may complete
bool mayComplete( TypeNode tn );
-
+
//for triggers
private:
/** helper function for compute var contains */
static Node getRewriteRule( Node q );
/** is fun def */
static bool isFunDef( Node q );
+ /** is fun def */
+ static bool isFunDefAnnotation( Node ipl );
/** is sygus conjecture */
static bool isSygusConjecture( Node q );
/** is sygus conjecture */
d_tr_trie = new inst::TriggerTrie;
d_hasAddedLemma = false;
- bool needsBuilder = false;
- bool needsRelDom = false;
Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
d_quant_rel = NULL;
}
+ d_qcf = NULL;
+ d_sg_gen = NULL;
+ d_inst_engine = NULL;
+ d_i_cbqi = NULL;
+ d_model_engine = NULL;
+ d_bint = NULL;
+ d_rr_engine = NULL;
+ d_ceg_inst = NULL;
+ d_lte_part_inst = NULL;
+ d_alpha_equiv = NULL;
+ d_fun_def_engine = NULL;
+ d_uee = NULL;
+ d_fs = NULL;
+ d_rel_dom = NULL;
+ d_builder = NULL;
+
+ d_total_inst_count_debug = 0;
+ d_ierCounter = 0;
+ d_ierCounter_lc = 0;
+ //if any strategy called only on last call, use phase 3
+ d_inst_when_phase = options::cbqi() ? 3 : 2;
+}
+
+QuantifiersEngine::~QuantifiersEngine(){
+ delete d_builder;
+ delete d_rr_engine;
+ delete d_bint;
+ delete d_model_engine;
+ delete d_inst_engine;
+ delete d_qcf;
+ delete d_quant_rel;
+ delete d_rel_dom;
+ delete d_model;
+ delete d_tr_trie;
+ delete d_term_db;
+ delete d_eq_query;
+ delete d_sg_gen;
+ delete d_ceg_inst;
+ delete d_lte_part_inst;
+ delete d_fun_def_engine;
+ delete d_uee;
+ delete d_fs;
+ delete d_i_cbqi;
+}
+
+EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
+ return d_eq_query;
+}
+
+context::Context* QuantifiersEngine::getSatContext(){
+ return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
+}
+
+context::UserContext* QuantifiersEngine::getUserContext(){
+ return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext();
+}
+
+OutputChannel& QuantifiersEngine::getOutputChannel(){
+ return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel();
+}
+/** get default valuation for the quantifiers engine */
+Valuation& QuantifiersEngine::getValuation(){
+ return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation();
+}
+
+void QuantifiersEngine::finishInit(){
+ context::Context * c = getSatContext();
+ Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl;
+ bool needsBuilder = false;
+ bool needsRelDom = false;
//add quantifiers modules
if( options::quantConflictFind() || options::quantRewriteRules() ){
d_qcf = new quantifiers::QuantConflictFind( this, c);
d_modules.push_back( d_qcf );
- }else{
- d_qcf = NULL;
}
if( options::conjectureGen() ){
d_sg_gen = new quantifiers::ConjectureGenerator( this, c );
d_modules.push_back( d_sg_gen );
- }else{
- d_sg_gen = NULL;
}
//maintain invariant : either InstantiationEngine or ModelEngine must be in d_modules
if( !options::finiteModelFind() || options::fmfInstEngine() ){
d_inst_engine = new quantifiers::InstantiationEngine( this );
d_modules.push_back( d_inst_engine );
- }else{
- d_inst_engine = NULL;
}
- //counterexample-based instantiation (initialized during finishInit)
- d_i_cbqi = NULL;
- if( options::cbqi() && options::cbqiModel() ){
- needsBuilder = true;
+ if( options::cbqi() ){
+ if( options::cbqiSplx() ){
+ d_i_cbqi = new quantifiers::InstStrategySimplex( (arith::TheoryArith*)getTheoryEngine()->theoryOf( THEORY_ARITH ), this );
+ d_modules.push_back( d_i_cbqi );
+ }else{
+ d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
+ d_modules.push_back( d_i_cbqi );
+ if( options::cbqiModel() ){
+ needsBuilder = true;
+ }
+ }
}
//finite model finding
if( options::finiteModelFind() ){
if( options::fmfBoundInt() ){
d_bint = new quantifiers::BoundedIntegers( c, this );
d_modules.push_back( d_bint );
- }else{
- d_bint = NULL;
}
d_model_engine = new quantifiers::ModelEngine( c, this );
d_modules.push_back( d_model_engine );
needsBuilder = true;
- }else{
- d_model_engine = NULL;
- d_bint = NULL;
}
if( options::quantRewriteRules() ){
d_rr_engine = new quantifiers::RewriteEngine( c, this );
d_modules.push_back(d_rr_engine);
- }else{
- d_rr_engine = NULL;
}
if( options::ceGuidedInst() ){
d_ceg_inst = new quantifiers::CegInstantiation( this, c );
d_modules.push_back( d_ceg_inst );
needsBuilder = true;
- }else{
- d_ceg_inst = NULL;
}
if( options::ltePartialInst() ){
d_lte_part_inst = new quantifiers::LtePartialInst( this, c );
d_modules.push_back( d_lte_part_inst );
- }else{
- d_lte_part_inst = NULL;
}
if( options::quantAlphaEquiv() ){
d_alpha_equiv = new quantifiers::AlphaEquivalence( this );
- }else{
- d_alpha_equiv = NULL;
}
//if( options::funDefs() ){
// d_fun_def_engine = new quantifiers::FunDefEngine( this, c );
// d_modules.push_back( d_fun_def_engine );
- //}else{
- d_fun_def_engine = NULL;
//}
if( options::quantEqualityEngine() ){
d_uee = new quantifiers::QuantEqualityEngine( this, c );
d_modules.push_back( d_uee );
- }else{
- d_uee = NULL;
}
//full saturation : instantiate from relevant domain, then arbitrary terms
if( options::fullSaturateQuant() || options::fullSaturateInst() ){
d_fs = new quantifiers::FullSaturation( this );
d_modules.push_back( d_fs );
needsRelDom = true;
- }else{
- d_fs = NULL;
}
if( needsRelDom ){
d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
- }else{
- d_rel_dom = NULL;
}
if( needsBuilder ){
Trace("quant-engine-debug") << "...make default model builder." << std::endl;
d_builder = new quantifiers::QModelBuilderDefault( c, this );
}
- }else{
- d_builder = NULL;
}
- d_total_inst_count_debug = 0;
- d_ierCounter = 0;
- d_ierCounter_lc = 0;
-}
-
-QuantifiersEngine::~QuantifiersEngine(){
- delete d_builder;
- delete d_rr_engine;
- delete d_bint;
- delete d_model_engine;
- delete d_inst_engine;
- delete d_qcf;
- delete d_quant_rel;
- delete d_rel_dom;
- delete d_model;
- delete d_tr_trie;
- delete d_term_db;
- delete d_eq_query;
- delete d_sg_gen;
- delete d_ceg_inst;
- delete d_lte_part_inst;
- delete d_fun_def_engine;
- delete d_uee;
- delete d_fs;
- delete d_i_cbqi;
-}
-
-EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
- return d_eq_query;
-}
-
-context::Context* QuantifiersEngine::getSatContext(){
- return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
-}
-
-context::Context* QuantifiersEngine::getUserContext(){
- return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext();
-}
-
-OutputChannel& QuantifiersEngine::getOutputChannel(){
- return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel();
-}
-/** get default valuation for the quantifiers engine */
-Valuation& QuantifiersEngine::getValuation(){
- return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation();
-}
-
-void QuantifiersEngine::finishInit(){
- Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl;
- //counterexample-based quantifier instantiation
- if( options::cbqi() ){
- if( options::cbqiSplx() ){
- d_i_cbqi = new quantifiers::InstStrategySimplex( (arith::TheoryArith*)getTheoryEngine()->theoryOf( THEORY_ARITH ), this );
- d_modules.push_back( d_i_cbqi );
- }else{
- d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
- d_modules.push_back( d_i_cbqi );
- }
- }else{
- d_i_cbqi = NULL;
- }
- for( int i=0; i<(int)d_modules.size(); i++ ){
- d_modules[i]->finishInit();
- }
}
QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
d_temp_inst_debug[f]++;
d_total_inst_count_debug++;
Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
- for( int i=0; i<(int)terms.size(); i++ ){
+ for( unsigned i=0; i<terms.size(); i++ ){
if( Trace.isOn("inst") ){
Trace("inst") << " " << terms[i];
if( Trace.isOn("inst-debug") ){
}
Trace("inst") << std::endl;
}
- Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) );
- }
- if( options::cbqiSplx() ){
- for( int i=0; i<(int)terms.size(); i++ ){
- if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){
+ if( options::cbqi() ){
+ if( quantifiers::TermDb::getInstConstAttr(terms[i])==f ){
Trace("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
- for( int i=0; i<(int)terms.size(); i++ ){
+ for( unsigned i=0; i<terms.size(); i++ ){
Trace("inst") << " " << terms[i] << std::endl;
}
Unreachable("Bad instantiation");
}
}
+ Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) );
}
if( options::instMaxLevel()!=-1 ){
uint64_t maxInstLevel = 0;
- for( int i=0; i<(int)terms.size(); i++ ){
+ for( unsigned i=0; i<terms.size(); i++ ){
if( terms[i].hasAttribute(InstLevelAttribute()) ){
if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
}else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){
performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
}else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){
- performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
+ performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase==0 ) || e==Theory::EFFORT_LAST_CALL );
}else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL ){
- performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
+ performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase==0 ) || e==Theory::EFFORT_LAST_CALL );
}else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){
performCheck = ( e >= Theory::EFFORT_LAST_CALL );
}else{
virtual ~QuantifiersModule(){}
//get quantifiers engine
QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
- /** initialize */
- virtual void finishInit() {}
/** presolve */
virtual void presolve() {}
/* whether this module needs to check this round */
/** inst round counters */
int d_ierCounter;
int d_ierCounter_lc;
+ int d_inst_when_phase;
/** has presolve been called */
context::CDO< bool > d_presolve;
/** presolve cache */
/** get default sat context for quantifiers engine */
context::Context* getSatContext();
/** get default sat context for quantifiers engine */
- context::Context* getUserContext();
+ context::UserContext* getUserContext();
/** get default output channel for the quantifiers engine */
OutputChannel& getOutputChannel();
/** get default valuation for the quantifiers engine */
fib-core.smt2 \
fore19-exp2-core.smt2 \
with-ind-104-core.smt2 \
- syn002-si-real-int.smt2
+ syn002-si-real-int.smt2 \
+ krs-sat.smt2
EXTRA_DIST = $(TESTS)
--- /dev/null
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-sort $$unsorted 0)
+(declare-fun cowlNothing ($$unsorted) Bool)
+(declare-fun cowlThing ($$unsorted) Bool)
+(declare-fun xsd_integer ($$unsorted) Bool)
+(declare-fun xsd_string ($$unsorted) Bool)
+(declare-fun is () $$unsorted)
+(assert (and (forall ((X $$unsorted)) (cowlThing X) ) (forall ((X $$unsorted)) (not (cowlNothing X)) )))
+(assert (forall ((X $$unsorted)) (= (xsd_string X) (not (xsd_integer X))) ))
+(assert (and (forall ((X $$unsorted)) (or (not (cowlThing X)) (= X is)) ) (cowlThing is)))
+(assert (cowlThing is))
+(assert (and (forall ((X $$unsorted)) (cowlThing X) ) (forall ((X $$unsorted)) (not (cowlNothing X)) ) (forall ((X $$unsorted)) (or (not (cowlThing X)) (= X is)) )))
+(check-sat)
floor.smt2 \
array-unsat-simp3.smt2 \
mix-simp.smt2 \
- mix-coeff.smt2 \
- mix-match.smt2
+ mix-coeff.smt2 \
+ mix-match.smt2 \
+ ari056.smt2
# regression can be solved with --finite-model-find --fmf-inst-engine
--- /dev/null
+(set-logic UFNIRA)
+(set-info :status unsat)
+(assert (forall ((X Int)) (= X 12) ))
+(check-sat)
projects / cvc5.git / commitdiff