summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.cpp40
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.cpp7
-rw-r--r--src/theory/quantifiers/term_database.cpp114
-rw-r--r--src/theory/quantifiers/term_database.h5
4 files changed, 113 insertions, 53 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index cae3e730e..8af11b1af 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -22,6 +22,7 @@
#include "theory/quantifiers/term_database.h"
#include "theory/theory_engine.h"
#include "prop/prop_engine.h"
+#include "theory/bv/theory_bv_rewriter.h"
using namespace CVC4::kind;
using namespace std;
@@ -56,12 +57,15 @@ void CegConjecture::assign( Node q ) {
}
}
d_quant = q;
+ Assert( d_candidates.empty() );
+ std::vector< Node > vars;
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ vars.push_back( q[0][i] );
d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) );
}
Trace("cegqi") << "Base quantified formula is : " << q << std::endl;
//construct base instantiation
- d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, d_candidates ) );
+ d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, vars, d_candidates ) );
Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){
CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj );
@@ -272,9 +276,26 @@ void CegInstantiation::preRegisterQuantifier( Node q ) {
if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
if( dt.isSygus() ){
- //take ownership of this quantified formula (will use direct evaluation instead of instantiation)
- d_quantEngine->setOwner( q, this );
- d_eval_axioms[q] = true;
+ //do unfolding if it induces Boolean structure,
+ //do direct evaluation if it does not induce Boolean structure,
+ // the reasoning is unfolding over these terms does not lead to helpful conflict analysis, and introduces many shared terms
+ bool directEval = true;
+ TypeNode ptn = pat.getType();
+ if( ptn.isBoolean() || ptn.isBitVector() ){
+ directEval = false;
+ }else{
+ unsigned cindex = Datatype::indexOf(pat[0].getOperator().toExpr() );
+ Node base = d_quantEngine->getTermDatabaseSygus()->getGenericBase( tn, dt, cindex );
+ Trace("cegqi-debug") << "Generic base term for " << pat[0] << " is " << base << std::endl;
+ if( base.getKind()==ITE ){
+ directEval = false;
+ }
+ }
+ if( directEval ){
+ //take ownership of this quantified formula (will use direct evaluation instead of unfolding instantiation)
+ d_quantEngine->setOwner( q, this );
+ d_eval_axioms[q] = true;
+ }
}
}
}
@@ -413,8 +434,13 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
}
if( !eager_eval_lem.empty() ){
for( unsigned j=0; j<eager_eval_lem.size(); j++ ){
- Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << eager_eval_lem[j] << std::endl;
- d_quantEngine->addLemma( eager_eval_lem[j] );
+ Node lem = eager_eval_lem[j];
+ if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){
+ //FIXME: hack to incorporate hacks from BV for division by zero
+ lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem );
+ }
+ Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl;
+ d_quantEngine->addLemma( lem );
}
return;
}
@@ -435,6 +461,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
}
}
//must get a counterexample to the value of the current candidate
+ Assert( conj->d_candidates.size()==model_values.size() );
Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
//check whether we will run CEGIS on inner skolem variables
bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 );
@@ -686,6 +713,7 @@ Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited )
}
Assert( subs[j-1].getType()==var_list[j-1].getType() );
}
+ Assert( vars.size()==subs.size() );
bTerm = bTerm.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl;
Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl;
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 33856d226..a5d4174dd 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -534,6 +534,7 @@ bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){
return false;
}else{
Trace("cegqi-engine") << siss.str() << std::endl;
+ Assert( d_single_inv_var.size()==subs.size() );
Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
if( d_qe->getTermDatabase()->containsVtsTerm( lem ) ){
Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl;
@@ -595,6 +596,7 @@ bool CegConjectureSingleInv::check( std::vector< Node >& lems ) {
for( unsigned i=0; i<d_sip->d_all_vars.size(); i++ ){
subs.push_back( NodeManager::currentNM()->mkSkolem( "kv", d_sip->d_all_vars[i].getType(), "created for verifying nsi" ) );
}
+ Assert( d_sip->d_all_vars.size()==subs.size() );
inst = inst.substitute( d_sip->d_all_vars.begin(), d_sip->d_all_vars.end(), subs.begin(), subs.end() );
Trace("cegqi-nsi") << "NSI : verification : " << inst << std::endl;
Trace("cegqi-lemma") << "Cegqi::Lemma : verification lemma : " << inst << std::endl;
@@ -751,6 +753,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
std::sort( indices.begin(), indices.end(), ssii );
Trace("csi-sol") << "Construct solution" << std::endl;
s = constructSolution( indices, sol_index, 0 );
+ Assert( vars.size()==d_sol->d_varList.size() );
s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() );
}
d_orig_solution = s;
@@ -922,6 +925,7 @@ void SingleInvocationPartition::process( Node n ) {
std::vector< Node > funcs;
//normalize the invocations
if( !terms.empty() ){
+ Assert( terms.size()==subs.size() );
cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
}
std::vector< Node > children;
@@ -940,6 +944,7 @@ void SingleInvocationPartition::process( Node n ) {
}
Trace("si-prt") << std::endl;
cr = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
+ Assert( terms.size()==subs.size() );
cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
Trace("si-prt-debug") << "...normalized invocations to " << cr << std::endl;
//now must check if it has other bound variables
@@ -974,6 +979,7 @@ void SingleInvocationPartition::process( Node n ) {
}
}
}
+ Assert( terms.size()==subs.size() );
cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
}
cr = Rewriter::rewrite( cr );
@@ -982,6 +988,7 @@ void SingleInvocationPartition::process( Node n ) {
TermDb::getBoundVars( cr, d_all_vars );
if( singleInvocation ){
//replace with single invocation formulation
+ Assert( si_terms.size()==si_subs.size() );
cr = cr.substitute( si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end() );
cr = Rewriter::rewrite( cr );
Trace("si-prt") << ".....si version=" << cr << std::endl;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index eff641736..e81245034 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -2480,8 +2480,8 @@ Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n );
if( it==d_sygus_to_builtin[tn].end() ){
Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl;
- Assert( n.getKind()==APPLY_CONSTRUCTOR );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Assert( n.getKind()==APPLY_CONSTRUCTOR );
unsigned i = Datatype::indexOf( n.getOperator().toExpr() );
Assert( n.getNumChildren()==dt[i].getNumArgs() );
std::map< TypeNode, int > var_count;
@@ -3200,9 +3200,17 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
}
}
+Node TermDbSygus::getAnchor( Node n ) {
+ if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+ return getAnchor( n[0] );
+ }else{
+ return n;
+ }
+}
+
void TermDbSygus::registerEvalTerm( Node n ) {
if( options::sygusDirectEval() ){
- if( n.getKind()==APPLY_UF ){
+ if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){
Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl;
TypeNode tn = n[0].getType();
if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
@@ -3210,58 +3218,72 @@ void TermDbSygus::registerEvalTerm( Node n ) {
if( dt.isSygus() ){
Node f = n.getOperator();
Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl;
- Assert( n[0].getKind()!=APPLY_CONSTRUCTOR );
- d_evals[n[0]].push_back( n );
- TypeNode tn = n[0].getType();
- Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Node var_list = Node::fromExpr( dt.getSygusVarList() );
- Assert( dt.isSygus() );
- d_eval_args[n[0]].push_back( std::vector< Node >() );
- for( unsigned j=1; j<n.getNumChildren(); j++ ){
- if( var_list[j-1].getType().isBoolean() ){
- //TODO: remove this case when boolean term conversion is eliminated
- Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
- d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) );
- }else{
- d_eval_args[n[0]].back().push_back( n[j] );
+ if( n[0].getKind()!=APPLY_CONSTRUCTOR ){
+ d_evals[n[0]].push_back( n );
+ TypeNode tn = n[0].getType();
+ Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Node var_list = Node::fromExpr( dt.getSygusVarList() );
+ Assert( dt.isSygus() );
+ d_eval_args[n[0]].push_back( std::vector< Node >() );
+ for( unsigned j=1; j<n.getNumChildren(); j++ ){
+ if( var_list[j-1].getType().isBoolean() ){
+ //TODO: remove this case when boolean term conversion is eliminated
+ Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+ d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) );
+ }else{
+ d_eval_args[n[0]].back().push_back( n[j] );
+ }
}
+ Node a = getAnchor( n[0] );
+ d_subterms[a][n[0]] = true;
}
-
}
}
}
}
}
-void TermDbSygus::registerModelValue( Node n, Node v, std::vector< Node >& lems ) {
- std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n );
- if( it!=d_eval_args.end() && !it->second.empty() ){
- unsigned start = d_node_mv_args_proc[n][v];
- Node antec = n.eqNode( v ).negate();
- TypeNode tn = n.getType();
- Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Assert( dt.isSygus() );
- Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << v << " for " << n << std::endl;
- Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl;
- Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( v, tn );
- Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl;
- std::vector< Node > vars;
- Node var_list = Node::fromExpr( dt.getSygusVarList() );
- for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
- vars.push_back( var_list[j] );
- }
- //for each evaluation
- for( unsigned i=start; i<it->second.size(); i++ ){
- Assert( vars.size()==it->second[i].size() );
- Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
- Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm );
- lem = NodeManager::currentNM()->mkNode( OR, antec, lem );
- Trace("sygus-eager") << "Lemma : " << lem << std::endl;
- lems.push_back( lem );
- }
- d_node_mv_args_proc[n][v] = it->second.size();
+void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems ) {
+ std::map< Node, std::map< Node, bool > >::iterator its = d_subterms.find( a );
+ if( its!=d_subterms.end() ){
+ Trace("sygus-eager") << "registerModelValue : " << a << ", has " << its->second.size() << " registered subterms." << std::endl;
+ for( std::map< Node, bool >::iterator itss = its->second.begin(); itss != its->second.end(); ++itss ){
+ Node n = itss->first;
+ Trace("sygus-eager-debug") << "...process : " << n << std::endl;
+ std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n );
+ if( it!=d_eval_args.end() && !it->second.empty() ){
+ TNode at = a;
+ TNode vt = v;
+ Node vn = n.substitute( at, vt );
+ vn = Rewriter::rewrite( vn );
+ unsigned start = d_node_mv_args_proc[n][vn];
+ Node antec = n.eqNode( vn ).negate();
+ TypeNode tn = n.getType();
+ Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Assert( dt.isSygus() );
+ Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << vn << " for " << n << std::endl;
+ Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl;
+ Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( vn, tn );
+ Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl;
+ std::vector< Node > vars;
+ Node var_list = Node::fromExpr( dt.getSygusVarList() );
+ for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
+ vars.push_back( var_list[j] );
+ }
+ //for each evaluation
+ for( unsigned i=start; i<it->second.size(); i++ ){
+ Assert( vars.size()==it->second[i].size() );
+ Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
+ Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm );
+ lem = NodeManager::currentNM()->mkNode( OR, antec, lem );
+ Trace("sygus-eager") << "Lemma : " << lem << std::endl;
+ lems.push_back( lem );
+ }
+ d_node_mv_args_proc[n][vn] = it->second.size();
+ }
+ }
}
}
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 4291587a4..b7b798cd4 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -557,7 +557,6 @@ public:
private:
std::map< TypeNode, std::map< int, Node > > d_generic_base;
std::map< TypeNode, std::vector< Node > > d_generic_templ;
- Node getGenericBase( TypeNode tn, const Datatype& dt, int c );
bool getMatch( Node p, Node n, std::map< int, Node >& s );
bool getMatch2( Node p, Node n, std::map< int, Node >& s, std::vector< int >& new_s );
public:
@@ -622,6 +621,7 @@ public:
/** get value */
Node getTypeMaxValue( TypeNode tn );
TypeNode getSygusTypeForVar( Node v );
+ Node getGenericBase( TypeNode tn, const Datatype& dt, int c );
Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
Node sygusToBuiltin( Node n, TypeNode tn );
Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 );
@@ -641,8 +641,11 @@ public:
/** print sygus term */
static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs );
+ /** get anchor */
+ static Node getAnchor( Node n );
//for eager instantiation
private:
+ std::map< Node, std::map< Node, bool > > d_subterms;
std::map< Node, std::vector< Node > > d_evals;
std::map< Node, std::vector< std::vector< Node > > > d_eval_args;
std::map< Node, std::map< Node, unsigned > > d_node_mv_args_proc;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback