PROOF(delete d_proofManager;);
PROOF(d_proofManager = NULL;);
-
+
delete d_stats;
d_stats = NULL;
delete d_statisticsRegistry;
if( !options::preSkolemQuant.wasSetByUser() ){
options::preSkolemQuant.set( true );
}
+ if( !options::preSkolemQuantNested.wasSetByUser() ){
+ options::preSkolemQuantNested.set( true );
+ }
if( !options::fmfOneInstPerRound.wasSetByUser() ){
options::fmfOneInstPerRound.set( true );
}
}
}
-
+
//apply counterexample guided instantiation options
if( options::cegqiSingleInv() ){
options::ceGuidedInst.set( true );
}
}
- //implied options...
+ //cbqi options
if( options::recurseCbqi() || options::cbqi2() ){
options::cbqi.set( true );
}
+ if( options::cbqi() ){
+ if( !options::quantConflictFind.wasSetByUser() ){
+ options::quantConflictFind.set( false );
+ }
+ }
+
+ //implied options...
if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
options::quantConflictFind.set( true );
}
Trace("smt") << "SmtEnginePrivate::addFormula(" << n << "), inUnsatCore = " << inUnsatCore << ", inInput = " << inInput << endl;
// Give it to proof manager
- PROOF(
+ PROOF(
if( inInput ){
// n is an input assertion
- ProofManager::currentPM()->addAssertion(n.toExpr(), inUnsatCore);
+ ProofManager::currentPM()->addAssertion(n.toExpr(), inUnsatCore);
}else{
// n is the result of an unknown preprocessing step, add it to dependency map to null
ProofManager::currentPM()->addDependence(n, Node::null());
SmtScope smts(this);
finalOptionsAreSet();
doPendingPops();
-
+
Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
// Substitute out any abstract values in ex
using namespace std;
namespace CVC4 {
-
+
CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ) : d_qe( qe ), d_out( out ){
-
-}
-
+ d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+ d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+ d_true = NodeManager::currentNM()->mkConst( true );
+}
+
void CegInstantiator::computeProgVars( Node n ){
if( d_prog_var.find( n )==d_prog_var.end() ){
d_prog_var[n].clear();
d_inelig[n] = true;
return;
}
+ if( d_has_delta.find( n[i] )!=d_has_delta.end() ){
+ d_has_delta[n] = true;
+ }
for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){
d_prog_var[n][it->first] = true;
}
}
+ if( n==d_n_delta ){
+ d_has_delta[n] = true;
+ }
}
}
-bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars,
+bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars,
std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
unsigned i, unsigned effort ){
if( i==d_vars.size() ){
//Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
Node pv = d_vars[i];
TypeNode pvtn = pv.getType();
-
+
if( (i+1)<d_vars.size() || effort!=2 ){
//[1] easy case : pv is in the equivalence class as another term not containing pv
if( ee->hasTerm( pv ) ){
while( !eqc_i.isFinished() ){
Node n = *eqc_i;
if( n!=pv ){
- Trace("cegqi-si-inst-debug") << i << "...try based on equal term " << n << std::endl;
+ Trace("cegqi-si-inst-debug") << "[1] " << i << "...try based on equal term " << n << std::endl;
//compute d_subs_fv, which program variables are contained in n
computeProgVars( n );
//must be an eligible term
ns = n;
proc = true;
}
+ if( d_has_delta.find( ns )!=d_has_delta.end() ){
+ //also must set delta to zero
+ ns = ns.substitute( (TNode)d_n_delta, (TNode)d_zero );
+ ns = Rewriter::rewrite( ns );
+ computeProgVars( ns );
+ }
if( proc ){
//try the substitution
subs_proc[0][ns][pv_coeff] = true;
++eqc_i;
}
}
-
+
//[2] : we can solve an equality for pv
///iterate over equivalence classes to find cases where we can solve for the variable
if( pvtn.isInteger() || pvtn.isReal() ){
for( unsigned j=0; j<lhs.size(); j++ ){
//if this term or the another has pv in it, try to solve for it
if( hasVar || lhs_v[j] ){
- Trace("cegqi-si-inst-debug") << i << "...try based on equality " << lhs[j] << " " << ns << std::endl;
+ Trace("cegqi-si-inst-debug") << "[2] " << i << "...try based on equality " << lhs[j] << " " << ns << std::endl;
Node eq_lhs = lhs[j];
Node eq_rhs = ns;
//make the same coefficient
Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl;
std::map< Node, Node > msum;
if( QuantArith::getMonomialSumLit( eq, msum ) ){
+ if( !d_n_delta.isNull() ){
+ msum.erase( d_n_delta );
+ }
if( Trace.isOn("cegqi-si-inst-debug") ){
Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl;
QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" );
++eqcs_i;
}
}
-
+
//[3] directly look at assertions
TheoryId tid = Theory::theoryOf( pv );
Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
bool pol = lit.getKind()!=NOT;
if( tid==THEORY_ARITH ){
if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){
- Assert( atom[1].isConst() );
- computeProgVars( atom[0] );
+ Assert( atom.getKind()!=GEQ || atom[1].isConst() );
+ Node atom_lhs;
+ Node atom_rhs;
+ if( atom.getKind()==GEQ ){
+ atom_lhs = atom[0];
+ atom_rhs = atom[1];
+ }else{
+ atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] );
+ atom_lhs = Rewriter::rewrite( atom_lhs );
+ atom_rhs = d_zero;
+ }
+
+ computeProgVars( atom_lhs );
//must be an eligible term
- if( d_inelig.find( atom[0] )==d_inelig.end() ){
+ if( d_inelig.find( atom_lhs )==d_inelig.end() ){
//apply substitution to LHS of atom
- Node atom_lhs;
- Node atom_rhs;
- if( !d_prog_var[atom[0]].empty() ){
+ if( !d_prog_var[atom_lhs].empty() ){
Node atom_lhs_coeff;
- atom_lhs = applySubstitution( atom[0], subs, vars, coeff, has_coeff, atom_lhs_coeff );
+ atom_lhs = applySubstitution( atom_lhs, subs, vars, coeff, has_coeff, atom_lhs_coeff );
if( !atom_lhs.isNull() ){
computeProgVars( atom_lhs );
- atom_rhs = atom[1];
if( !atom_lhs_coeff.isNull() ){
atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) );
}
}
- }else{
- atom_lhs = atom[0];
- atom_rhs = atom[1];
}
//if it contains pv
if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){
Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
- Trace("cegqi-si-inst-debug") << "From assertion : " << atom << ", pol = " << pol << std::endl;
- Trace("cegqi-si-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl;
+ Trace("cegqi-si-inst-debug") << "[3] From assertion : " << atom << ", pol = " << pol << std::endl;
+ Trace("cegqi-si-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl;
std::map< Node, Node > msum;
if( QuantArith::getMonomialSumLit( satom, msum ) ){
+ if( !d_n_delta.isNull() ){
+ msum.erase( d_n_delta );
+ }
if( Trace.isOn("cegqi-si-inst-debug") ){
Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl;
QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" );
if( addInstantiationInc( uval, pv, veq_c, uires, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){
return true;
}
+ }else{
+ Trace("cegqi-si-inst-debug") << "...already processed." << std::endl;
}
}
}
}
}
}
-
- //[4] resort to using value in model
+
+ //[4] resort to using value in model
if( effort>0 ){
Node mv = d_qe->getModel()->getValue( pv );
Node pv_coeff_m;
- Trace("cegqi-si-inst-debug") << i << "...try model value " << mv << std::endl;
+ Trace("cegqi-si-inst-debug") << i << "[4] ...try model value " << mv << std::endl;
return addInstantiationInc( mv, pv, pv_coeff_m, 9, subs, vars, coeff, has_coeff, subs_typ, i, 1 );
}else{
return false;
}
-bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars,
+bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars,
std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
- unsigned i, unsigned effort ) {
+ unsigned i, unsigned effort ) {
//must ensure variables have been computed for n
computeProgVars( n );
//substitute into previous substitutions, when applicable
a_coeff.push_back( pv_coeff );
a_has_coeff.push_back( pv );
}
-
+
bool success = true;
std::map< int, Node > prev_subs;
std::map< int, Node > prev_coeff;
}
}
-bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars,
+bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars,
std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned j ) {
if( j==has_coeff.size() ){
return addInstantiation( subs, vars, subs_typ );
if( !veq_c.isNull() ){
subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c );
if( subs_typ[index]>=1 && subs_typ[index]<=2 ){
- subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index],
- NodeManager::currentNM()->mkNode( ITE,
- NodeManager::currentNM()->mkNode( EQUAL,
- NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
- NodeManager::currentNM()->mkConst( Rational( 0 ) ) ),
- NodeManager::currentNM()->mkConst( Rational( 0 ) ),
- NodeManager::currentNM()->mkConst( Rational( 1 ) ) )
+ subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index],
+ NodeManager::currentNM()->mkNode( ITE,
+ NodeManager::currentNM()->mkNode( EQUAL,
+ NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
+ d_zero ),
+ d_zero, d_one )
);
}
}
//equalities are both upper and lower bounds
/*
if( subs_typ[index]==0 && !veq_c.isNull() ){
- subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index],
- NodeManager::currentNM()->mkNode( ITE,
- NodeManager::currentNM()->mkNode( EQUAL,
- NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
+ subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index],
+ NodeManager::currentNM()->mkNode( ITE,
+ NodeManager::currentNM()->mkNode( EQUAL,
+ NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
NodeManager::currentNM()->mkConst( Rational( 0 ) ) ),
NodeManager::currentNM()->mkConst( Rational( 0 ) ),
NodeManager::currentNM()->mkConst( Rational( 1 ) ) )
prev[i] = subs[i];
if( d_n_delta.isNull() ){
d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", vars[i].getType(), "delta for cegqi" );
- Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) );
+ Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, d_zero );
d_qe->getOutputChannel().lemma( delta_lem );
}
subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta );
}
-Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars,
+Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars,
std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff ) {
Assert( d_prog_var.find( n )!=d_prog_var.end() );
Assert( n==Rewriter::rewrite( n ) );
}
}
+//check if delta has a lower bound L
+// if so, add lemma L>0 => L>d
+void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) {
+ if( !d_n_delta.isNull() ){
+ Theory* theory = d_qe->getTheoryEngine()->theoryOf( THEORY_ARITH );
+ if( theory && d_qe->getTheoryEngine()->isTheoryEnabled( THEORY_ARITH ) ){
+ context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
+ for (unsigned j = 0; it != it_end; ++ it, ++j) {
+ Node lit = (*it).assertion;
+ Node atom = lit.getKind()==NOT ? lit[0] : lit;
+ bool pol = lit.getKind()!=NOT;
+ if( atom.getKind()==GEQ || ( pol && atom.getKind()==EQUAL ) ){
+ Assert( atom.getKind()!=GEQ || atom[1].isConst() );
+ Node atom_lhs;
+ Node atom_rhs;
+ if( atom.getKind()==GEQ ){
+ atom_lhs = atom[0];
+ atom_rhs = atom[1];
+ }else{
+ atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] );
+ atom_lhs = Rewriter::rewrite( atom_lhs );
+ atom_rhs = d_zero;
+ }
+ computeProgVars( atom_lhs );
+ //must be an eligible term with delta
+ if( d_inelig.find( atom_lhs )==d_inelig.end() && d_has_delta.find( atom_lhs )!=d_has_delta.end() ){
+ Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
+ Trace("cegqi-delta") << "Delta assertion : " << atom << ", pol = " << pol << std::endl;
+ std::map< Node, Node > msum;
+ if( QuantArith::getMonomialSumLit( satom, msum ) ){
+ Node vatom;
+ //isolate delta in the inequality
+ int ires = QuantArith::isolate( d_n_delta, msum, vatom, atom.getKind(), true );
+ if( ((ires==1)==pol) || ( ires!=0 && lit.getKind()==EQUAL ) ){
+ Node val = vatom[ ires==1 ? 1 : 0 ];
+ Node pvm = vatom[ ires==1 ? 0 : 1 ];
+ //get monomial
+ if( pvm!=d_n_delta ){
+ Node veq_c;
+ Node veq_v;
+ if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
+ Assert( veq_v==d_n_delta );
+ val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
+ val = Rewriter::rewrite( val );
+ }else{
+ val = Node::null();
+ }
+ }
+ if( !val.isNull() ){
+ Node lem1 = NodeManager::currentNM()->mkNode( GT, val, d_zero );
+ lem1 = Rewriter::rewrite( lem1 );
+ if( !lem1.isConst() || lem1==d_true ){
+ Node lem2 = NodeManager::currentNM()->mkNode( GT, val, d_n_delta );
+ Node lem = lem1==d_true ? lem2 : NodeManager::currentNM()->mkNode( OR, lem1.negate(), lem2 );
+ lems.push_back( lem );
+ Trace("cegqi-delta") << "...lemma : " << lem << std::endl;
+ }
+ }
+ }else{
+ Trace("cegqi-delta") << "...wrong polarity." << std::endl;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
void CegInstantiator::check() {
+
for( unsigned r=0; r<2; r++ ){
std::vector< Node > subs;
std::vector< Node > vars;
}
Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
}
-
-
+
+
bool CegqiOutputSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) {
return d_out->addInstantiation( subs, subs_typ );
}
-
+
bool CegqiOutputSingleInv::isEligibleForInstantiation( Node n ) {
return d_out->isEligibleForInstantiation( n );
-}
-
-
-
+}
+
+bool CegqiOutputSingleInv::addLemma( Node n ) {
+ return d_out->addLemma( n );
+}
+
+
CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent( p ){
d_sol = NULL;
d_c_inst_match_trie = NULL;
Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
inst = TermDb::simpleNegate( inst );
Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
-
+
//initialize the instantiator for this
CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
d_cinst = new CegInstantiator( d_qe, cosi );
d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
-
+
return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
}else{
return Node::null();
return n.getKind()!=SKOLEM || std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end();
}
+bool CegConjectureSingleInv::addLemma( Node n ) {
+ d_curr_lemmas.push_back( n );
+ return true;
+}
+
void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
if( !d_single_inv.isNull() ) {
Assert( d_cinst!=NULL );
d_curr_lemmas.clear();
- //call check for instantiator
- d_cinst->check();
- //add lemmas
- lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() );
+ //check if there are delta lemmas
+ d_cinst->getDeltaLemmas( d_curr_lemmas );
+ //if not, do ce-guided instantiation
+ if( d_curr_lemmas.empty() ){
+ //call check for instantiator
+ d_cinst->check();
+ //add lemmas
+ lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() );
+ }
}
}
public:
virtual bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) = 0;
virtual bool isEligibleForInstantiation( Node n ) = 0;
+ virtual bool addLemma( Node lem ) = 0;
};
class CegInstantiator
{
private:
+ Node d_zero;
+ Node d_one;
+ Node d_true;
QuantifiersEngine * d_qe;
CegqiOutput * d_out;
//program variable contains cache
std::map< Node, std::map< Node, bool > > d_prog_var;
std::map< Node, bool > d_inelig;
+ std::map< Node, bool > d_has_delta;
private:
- Node d_n_delta;
//for adding instantiations during check
void computeProgVars( Node n );
// effort=0 : do not use model value, 1: use model value, 2: one must use model value
- bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars,
+ bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars,
std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
unsigned i, unsigned effort );
- bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars,
+ bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars,
std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
unsigned i, unsigned effort );
- bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars,
+ bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars,
std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
unsigned j );
bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ );
- Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars,
- std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true );
+ Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars,
+ std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true );
public:
CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out );
//the CE variables
std::vector< Node > d_vars;
+ //delta
+ Node d_n_delta;
+ //check : add instantiations based on valuation of d_vars
void check();
+ // get delta lemmas : on-demand force minimality of d_n_delta
+ void getDeltaLemmas( std::vector< Node >& lems );
};
CegConjectureSingleInv * d_out;
bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
bool isEligibleForInstantiation( Node n );
+ bool addLemma( Node lem );
};
bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
//is eligible for instantiation
bool isEligibleForInstantiation( Node n );
+ // add lemma
+ bool addLemma( Node lem );
public:
CegConjectureSingleInv( CegConjecture * p );
// original conjecture
Node n = assertions[i][1][0];
Assert( n.getKind()==APPLY_UF );
Node f = n.getOperator();
-
+
//check if already defined, if so, throw error
if( d_sorts.find( f )!=d_sorts.end() ){
Message() << "Cannot define function " << f << " more than once." << std::endl;
exit( 0 );
}
-
+
//create a sort S that represents the inputs of the function
std::stringstream ss;
ss << "I_" << f;
TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() );
d_sorts[f] = iType;
-
+
//create functions f1...fn mapping from this sort to concrete elements
for( unsigned j=0; j<n.getNumChildren(); j++ ){
TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() );
ss << f << "_arg_" << j;
d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) );
}
-
+
//construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn]
std::vector< Node > children;
Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType );
subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) );
}
Node bd = assertions[i][1].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-
+
Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl;
Trace("fmf-fun-def") << " to " << std::endl;
assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
}
//second pass : rewrite assertions
for( unsigned i=0; i<assertions.size(); i++ ){
- bool is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end();
+ int is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end() ? 1 : 0;
std::vector< Node > constraints;
+ Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl;
Node n = simplify( assertions[i], true, true, constraints, is_fd );
Assert( constraints.empty() );
if( n!=assertions[i] ){
}
}
-Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, bool is_fun_def ) {
+Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def ) {
Trace("fmf-fun-def-debug") << "Simplify " << n << " " << pol << " " << hasPol << " " << is_fun_def << std::endl;
if( n.getKind()==FORALL ){
Node c = simplify( n[1], pol, hasPol, constraints, is_fun_def );
}else{
return n;
}
- }else if( n.getType().isBoolean() && n.getKind()!=APPLY_UF ){
- std::vector< Node > children;
- bool childChanged = false;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node c = n[i];
- //do not process LHS of definition
- if( !is_fun_def || i!=0 ){
- bool newHasPol;
- bool newPol;
- QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
- //get child constraints
- std::vector< Node > cconstraints;
- c = simplify( n[i], newPol, newHasPol, cconstraints );
- constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() );
+ }else{
+ Node nn = n;
+ bool isBool = n.getType().isBoolean();
+ if( isBool && n.getKind()!=APPLY_UF && is_fun_def!=2 ){
+ std::vector< Node > children;
+ bool childChanged = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node c = n[i];
+ //do not process LHS of definition
+ if( is_fun_def!=1 || i!=0 ){
+ bool newHasPol;
+ bool newPol;
+ QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+ //get child constraints
+ std::vector< Node > cconstraints;
+ c = simplify( n[i], newPol, newHasPol, cconstraints, is_fun_def==1 ? 2 : 0 );
+ constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() );
+ }
+ children.push_back( c );
+ childChanged = c!=n[i] || childChanged;
}
- children.push_back( c );
- childChanged = c!=n[i] || childChanged;
- }
- if( !constraints.empty() || childChanged ){
- std::vector< Node > c;
if( childChanged ){
- c.push_back( NodeManager::currentNM()->mkNode( n.getKind(), children ) );
- }else{
- c.push_back( n );
+ nn = n;
}
- if( hasPol ){
- //conjoin with current
- for( unsigned i=0; i<constraints.size(); i++ ){
- if( pol ){
- c.push_back( constraints[i] );
- }else{
- c.push_back( constraints[i].negate() );
- }
+ }else{
+ //simplify term
+ simplifyTerm( n, constraints );
+ }
+ if( !constraints.empty() && isBool && hasPol ){
+ std::vector< Node > c;
+ c.push_back( nn );
+ //conjoin with current
+ for( unsigned i=0; i<constraints.size(); i++ ){
+ if( pol ){
+ c.push_back( constraints[i] );
+ }else{
+ c.push_back( constraints[i].negate() );
}
- constraints.clear();
- }else{
- //must add at higher level
}
+ constraints.clear();
return c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( pol ? AND : OR, c );
+ }else{
+ return nn;
}
- }else{
- //simplify term
- simplifyTerm( n, constraints );
}
- return n;
}
void FunDefFmf::simplifyTerm( Node n, std::vector< Node >& constraints ) {
//defined functions to injections input -> argument elements
std::map< Node, std::vector< Node > > d_input_arg_inj;
//simplify
- Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, bool is_fun_def = false );
+ Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def = 0 );
//simplify term
void simplifyTerm( Node n, std::vector< Node >& constraints );
public:
return d_out->isEligibleForInstantiation( n );
}
+bool CegqiOutputInstStrategy::addLemma( Node lem ) {
+ return d_out->addLemma( lem );
+}
+
InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( qe ) {
d_out = new CegqiOutputInstStrategy( this );
}
void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
-
+ d_check_delta_lemma = true;
}
int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f );
if( it==d_cinst.end() ){
cinst = new CegInstantiator( d_quantEngine, d_out );
+ if( d_n_delta.isNull() ){
+ d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for cegqi inst strategy" );
+ Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) );
+ d_quantEngine->getOutputChannel().lemma( delta_lem );
+ }
+ cinst->d_n_delta = d_n_delta;
for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) );
}
}else{
cinst = it->second;
}
+ if( d_check_delta_lemma ){
+ Trace("inst-alg") << "-> Get delta lemmas for cegqi..." << std::endl;
+ d_check_delta_lemma = false;
+ std::vector< Node > dlemmas;
+ cinst->getDeltaLemmas( dlemmas );
+ Trace("inst-alg") << "...got " << dlemmas.size() << " delta lemmas." << std::endl;
+ if( !dlemmas.empty() ){
+ bool addedLemma = false;
+ for( unsigned i=0; i<dlemmas.size(); i++ ){
+ if( addLemma( dlemmas[i] ) ){
+ addedLemma = true;
+ }
+ }
+ if( addedLemma ){
+ return STATUS_UNKNOWN;
+ }
+ }
+ }
+ Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
d_curr_quant = f;
cinst->check();
d_curr_quant = Node::null();
-
- return STATUS_UNKNOWN;
- }else{
- // To fix warning
- Unreachable();
}
+ return STATUS_UNKNOWN;
}
bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) {
Assert( !d_curr_quant.isNull() );
+ /*
+ std::stringstream siss;
+ if( Trace.isOn("inst-cegqi") || Trace.isOn("inst-cegqi-debug") ){
+ for( unsigned j=0; j<d_single_inv_sk.size(); j++ ){
+ Node v = d_single_inv_map_to_prog[d_single_inv[0][j]];
+ siss << " * " << v;
+ siss << " (" << d_single_inv_sk[j] << ")";
+ siss << " -> " << ( subs_typ[j]==9 ? "M:" : "") << subs[j] << std::endl;
+ }
+ }
+ */
return d_quantEngine->addInstantiation( d_curr_quant, subs, false );
}
+bool InstStrategyCegqi::addLemma( Node lem ) {
+ return d_quantEngine->addLemma( lem );
+}
+
bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
- return true;
+ if( n.getKind()==INST_CONSTANT ){
+ //only legal if current quantified formula contains n
+ return TermDb::containsTerm( d_curr_quant, n );
+ }else{
+ return true;
+ }
}
InstStrategyCegqi * d_out;
bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
bool isEligibleForInstantiation( Node n );
+ bool addLemma( Node lem );
};
class InstStrategyCegqi : public InstStrategy {
private:
CegqiOutputInstStrategy * d_out;
std::map< Node, CegInstantiator * > d_cinst;
+ Node d_n_delta;
Node d_curr_quant;
+ bool d_check_delta_lemma;
/** process functions */
void processResetInstantiationRound( Theory::Effort effort );
int process( Node f, Theory::Effort effort, int e );
bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
bool isEligibleForInstantiation( Node n );
+ bool addLemma( Node lem );
/** identify */
std::string identify() const { return std::string("Cegqi"); }
};
//check each instantiation strategy
for( size_t i=0; i<d_instStrategies.size(); ++i ){
InstStrategy* is = d_instStrategies[i];
- Debug("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
+ Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
int quantStatus = is->process( f, effort, e_use );
- Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
+ Trace("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
finished = false;
}
<< d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
+ Debug("quantifiers") << "Process " << n << "..." << std::endl;
//it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
if( !d_quantEngine->hasOwnership( n, this ) ){
d_quant_active[n] = false;
+ Debug("quantifiers") << " Quantifier has owner." << std::endl;
}else if( !d_quantEngine->getModel()->isQuantifierActive( n ) ){
d_quant_active[n] = false;
+ Debug("quantifiers") << " Quantifier is not active (from model)." << std::endl;
//it is not active if we have found the skolemized negation is unsat
}else if( options::cbqi() && hasAddedCbqiLemma( n ) ){
Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n );
# forall x. P( x ) => f( S( x ) ) = x
option preSkolemQuant --pre-skolem-quant bool :read-write :default false
apply skolemization eagerly to bodies of quantified formulas
+option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true
+ apply skolemization to nested quantified formulass
+option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true
+ apply skolemization to quantified formulas aggressively
# Whether to perform agressive miniscoping
option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
perform aggressive miniscoping for quantifiers
}else{
std::vector< Node > children;
Kind k = body[0].getKind();
-
+
if( body[0].getKind()==OR || body[0].getKind()==AND ){
k = body[0].getKind()==AND ? OR : AND;
for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
return nn.negate();
}else if( n.getKind()==kind::FORALL ){
if( polarity ){
- if( options::preSkolemQuant() ){
+ if( options::preSkolemQuant() && ( options::preSkolemQuantNested() || fvs.empty() ) ){
vector< Node > children;
children.push_back( n[0] );
//add children to current scope
if( containsQuantifiers( n ) ){
if( n.getType().isBoolean() ){
if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
- Node nn;
- //must remove structure
- if( n.getKind()==kind::ITE ){
- nn = NodeManager::currentNM()->mkNode( kind::AND,
- NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
- NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
- }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
- nn = NodeManager::currentNM()->mkNode( kind::AND,
- NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
- NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
- }else if( n.getKind()==kind::IMPLIES ){
- nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
+ if( options::preSkolemQuantAgg() ){
+ Node nn;
+ //must remove structure
+ if( n.getKind()==kind::ITE ){
+ nn = NodeManager::currentNM()->mkNode( kind::AND,
+ NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
+ NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
+ }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
+ nn = NodeManager::currentNM()->mkNode( kind::AND,
+ NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
+ NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
+ }else if( n.getKind()==kind::IMPLIES ){
+ nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
+ }
+ return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
}
- return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
}else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
vector< Node > children;
for( int i=0; i<(int)n.getNumChildren(); i++ ){
Trace("quant") << " : " << f << std::endl;
++(d_statistics.d_num_quant);
Assert( f.getKind()==FORALL );
-
+
//check whether we should apply a reduction
bool reduced = false;
if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){
Trace("inst") << std::endl;
Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) );
}
- if( options::cbqi() ){
+ if( options::cbqi() && !options::cbqi2() ){
for( int i=0; i<(int)terms.size(); i++ ){
if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){
Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
}
setInstantiationLevelAttr( body, f[1], maxInstLevel+1 );
}
- Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
++(d_statistics.d_instantiations);
return true;
}else{
Trace("partial-inst") << "Partial instantiation : " << f << std::endl;
Trace("partial-inst") << " : " << body << std::endl;
}else{
- //do optimized version
- Node icb = d_term_db->getInstConstantBody( f );
- body = getSubstitute( icb, terms );
- if( Debug.isOn("check-inst") ){
- Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
- if( body!=body2 ){
- Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
+ if( options::cbqi() ){
+ body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+ }else{
+ //do optimized version
+ Node icb = d_term_db->getInstConstantBody( f );
+ body = getSubstitute( icb, terms );
+ if( Debug.isOn("check-inst") ){
+ Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+ if( body!=body2 ){
+ Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
+ }
}
}
}
bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
if( doCache ){
- Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
lem = Rewriter::rewrite(lem);
+ Trace("inst-add-debug2") << "Adding lemma : " << lem << std::endl;
if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
//d_curr_out->lemma( lem, false, true );
d_lemmas_produced_c[ lem ] = true;
d_lemmas_waiting.push_back( lem );
- Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl;
+ Trace("inst-add-debug2") << "Added lemma : " << lem << std::endl;
return true;
}else{
- Debug("inst-engine-debug") << "Duplicate." << std::endl;
+ Trace("inst-add-debug2") << "Duplicate." << std::endl;
return false;
}
}else{
out << "Internal error : module for synth solution not found." << std::endl;
}
}
-
+
QuantifiersEngine::Statistics::Statistics():
d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
projects / cvc5.git / commitdiff