summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ceg_instantiator.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/ceg_instantiator.cpp')
-rw-r--r--src/theory/quantifiers/ceg_instantiator.cpp62
1 files changed, 41 insertions, 21 deletions
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index e4d12904e..d31851ec4 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -20,6 +20,7 @@
#include "theory/arith/theory_arith_private.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/theory_engine.h"
#include "theory/bv/theory_bv_utils.h"
@@ -372,7 +373,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
int ires = solve_arith( pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta );
if( ires!=0 ){
//disequalities are either strict upper or lower bounds
- unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2;
+ unsigned rmax = ( atom.getKind()==GEQ || options::cbqiModel() ) ? 1 : 2;
for( unsigned r=0; r<rmax; r++ ){
int uires = ires;
Node uval = val;
@@ -390,7 +391,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
}
}
}else{
- bool is_upper = ( r==0 );
+ bool is_upper;
if( options::cbqiModel() ){
// disequality is a disjunction : only consider the bound in the direction of the model
//first check if there is an infinity...
@@ -413,6 +414,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
Assert( cmp.isConst() );
is_upper = ( cmp!=d_true );
}
+ }else{
+ is_upper = (r==0);
}
Assert( atom.getKind()==EQUAL && !pol );
if( pvtn.isInteger() ){
@@ -450,6 +453,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
unsigned index = uires>0 ? 0 : 1;
mbp_bounds[index].push_back( uval );
mbp_coeff[index].push_back( veq_c );
+ Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << veq_c << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl;
for( unsigned t=0; t<2; t++ ){
mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta );
}
@@ -719,6 +723,13 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
//[5] 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() || pvtn.isBitVector() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){
+
+#ifdef CVC4_ASSERTIONS
+ if( pvtn.isReal() && options::cbqiNestedQE() && !options::cbqiAll() ){
+ Trace("cbqi-warn") << "Had to resort to model value." << std::endl;
+ Assert( false );
+ }
+#endif
Node mv = getModelValue( pv );
Node pv_coeff_m;
Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl;
@@ -1222,25 +1233,27 @@ void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& ter
}
void CegInstantiator::presolve( Node q ) {
- Trace("cbqi-presolve") << "CBQI presolve " << q << std::endl;
//at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing
- std::vector< Node > vars;
- std::map< Node, std::vector< Node > > teq;
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- vars.push_back( q[0][i] );
- teq[q[0][i]].clear();
- }
- collectPresolveEqTerms( q[1], teq );
- std::vector< Node > terms;
- std::vector< Node > conj;
- getPresolveEqConjuncts( vars, terms, teq, q, conj );
+ //only if no nested quantifiers
+ if( !QuantifiersRewriter::containsQuantifiers( q[1] ) ){
+ std::vector< Node > vars;
+ std::map< Node, std::vector< Node > > teq;
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ vars.push_back( q[0][i] );
+ teq[q[0][i]].clear();
+ }
+ collectPresolveEqTerms( q[1], teq );
+ std::vector< Node > terms;
+ std::vector< Node > conj;
+ getPresolveEqConjuncts( vars, terms, teq, q, conj );
- if( !conj.empty() ){
- Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
- Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
- lem = NodeManager::currentNM()->mkNode( OR, g, lem );
- Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl;
- d_qe->getOutputChannel().lemma( lem, false, true );
+ if( !conj.empty() ){
+ Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
+ Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
+ lem = NodeManager::currentNM()->mkNode( OR, g, lem );
+ Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl;
+ d_qe->getOutputChannel().lemma( lem, false, true );
+ }
}
}
@@ -1479,7 +1492,8 @@ struct sortCegVarOrder {
void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
- Assert( d_vars.empty() );
+ //Assert( d_vars.empty() );
+ d_vars.clear();
d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
//determine variable order: must do Reals before Ints
@@ -1512,7 +1526,9 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
//remove ITEs
IteSkolemMap iteSkolemMap;
d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
- Assert( d_aux_vars.empty() );
+ //Assert( d_aux_vars.empty() );
+ d_aux_vars.clear();
+ d_aux_eq.clear();
for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
Trace("cbqi-debug") << " Auxiliary var (from ITE) : " << i->first << std::endl;
d_aux_vars.push_back( i->first );
@@ -1601,6 +1617,7 @@ int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, No
if( options::cbqiAll() ){
// when not pure LIA/LRA, we must check whether the lhs contains pv
if( TermDb::containsTerm( val, pv ) ){
+ Trace("cbqi-inst-debug") << "fail : contains bad term" << std::endl;
return 0;
}
}
@@ -1656,6 +1673,9 @@ int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, No
}
vts_coeff_inf = vts_coeff[0];
vts_coeff_delta = vts_coeff[1];
+ Trace("cbqi-inst-debug") << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" << std::endl;
+ }else{
+ Trace("cbqi-inst-debug") << "fail : could not get monomial sum" << std::endl;
}
return ires;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback