summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/quantifiers/ceg_instantiator.cpp13
-rw-r--r--src/theory/quantifiers/ceg_t_instantiator.cpp239
-rw-r--r--src/theory/quantifiers/ceg_t_instantiator.h82
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.cpp3
-rw-r--r--src/theory/quantifiers/term_database.cpp6
-rw-r--r--src/theory/quantifiers/term_database.h3
-rw-r--r--src/theory/quantifiers_engine.cpp10
-rw-r--r--src/theory/quantifiers_engine.h13
-rw-r--r--test/regress/regress0/quantifiers/Makefile.am8
-rw-r--r--test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt23
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-mul.smt22
11 files changed, 262 insertions, 120 deletions
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 0386a0fdb..2fdc37134 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -55,7 +55,6 @@ void CegInstantiator::computeProgVars( Node n ){
computeProgVars( n[i] );
if( d_inelig.find( n[i] )!=d_inelig.end() ){
d_inelig[n] = true;
- return;
}
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;
@@ -126,7 +125,6 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
if( needsPostprocess ){
//must make copy so that backtracking reverts sf
SolvedForm sf_tmp = sf;
- unsigned prev_var_size = sf.d_vars.size();
bool postProcessSuccess = true;
for( std::map< Instantiator *, Node >::iterator itp = pp_inst_to_var.begin(); itp != pp_inst_to_var.end(); ++itp ){
if( !itp->first->postProcessInstantiationForVariable( this, sf_tmp, itp->second, effort, lemmas ) ){
@@ -134,17 +132,6 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
break;
}
}
- if( sf_tmp.d_vars.size()>prev_var_size ){
- // if we added substitutions during postprocess, process these now
- std::vector< Node > new_vars;
- std::vector< Node > new_subs;
- for( unsigned i=0; i<prev_var_size; i++ ){
- Node subs = sf_tmp.d_subs[i];
- sf_tmp.d_subs[i] = subs.substitute( sf_tmp.d_vars.begin() + prev_var_size, sf_tmp.d_vars.end(),
- sf_tmp.d_subs.begin() + prev_var_size, sf_tmp.d_subs.end() );
- }
- }
-
if( postProcessSuccess ){
return doAddInstantiation( sf_tmp.d_vars, sf_tmp.d_subs, lemmas );
}else{
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 75118dadc..e2065ffd9 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -26,6 +26,8 @@
#include "theory/bv/theory_bv_utils.h"
#include "util/bitvector.h"
+#include <algorithm>
+
using namespace std;
using namespace CVC4;
using namespace CVC4::kind;
@@ -834,7 +836,18 @@ bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, N
Node BvInverter::getSolveVariable( TypeNode tn ) {
std::map< TypeNode, Node >::iterator its = d_solve_var.find( tn );
if( its==d_solve_var.end() ){
- Node k = NodeManager::currentNM()->mkSkolem( "s", tn );
+ std::stringstream ss;
+ if( tn.isFunction() ){
+ Assert( tn.getNumChildren()==2 );
+ Assert( tn[0].isBoolean() );
+ ss << "slv_f";
+ }else{
+ ss << "slv";
+ }
+ Node k = NodeManager::currentNM()->mkSkolem( ss.str(), tn );
+ // marked as a virtual term (it is eligible for instantiation)
+ VirtualTermSkolemAttribute vtsa;
+ k.setAttribute(vtsa,true);
d_solve_var[tn] = k;
return k;
}else{
@@ -843,10 +856,31 @@ Node BvInverter::getSolveVariable( TypeNode tn ) {
}
Node BvInverter::getInversionSkolemFor( Node cond, TypeNode tn ) {
+ // condition should be rewritten
+ Assert( Rewriter::rewrite(cond)==cond );
std::unordered_map< Node, Node, NodeHashFunction >::iterator it = d_inversion_skolem_cache.find( cond );
if( it==d_inversion_skolem_cache.end() ){
- Node skv = NodeManager::currentNM()->mkSkolem ("skvinv", tn, "created for BvInverter");
- Trace("cegqi-bv-skvinv") << "SKVINV : " << skv << " is the skolem associated with conditon " << cond << std::endl;
+ Node skv;
+ if( cond.getKind()==EQUAL ){
+ // optimization : if condition is ( x = v ) should just return v and not introduce a Skolem
+ // this can happen when we ask for the multiplicative inversion with bv1
+ Node x = getSolveVariable( tn );
+ for( unsigned i=0; i<2; i++ ){
+ if( cond[i]==x ){
+ skv = cond[1-i];
+ Trace("cegqi-bv-skvinv") << "SKVINV : " << skv << " is trivially associated with conditon " << cond << std::endl;
+ break;
+ }
+ }
+ }
+ if( skv.isNull() ){
+ // TODO : compute the value if the condition is deterministic, e.g. calc multiplicative inverse of 2 constants
+ skv = NodeManager::currentNM()->mkSkolem ("skvinv", tn, "created for BvInverter");
+ Trace("cegqi-bv-skvinv") << "SKVINV : " << skv << " is the skolem associated with conditon " << cond << std::endl;
+ // marked as a virtual term (it is eligible for instantiation)
+ VirtualTermSkolemAttribute vtsa;
+ skv.setAttribute(vtsa,true);
+ }
d_inversion_skolem_cache[cond] = skv;
return skv;
}else{
@@ -855,27 +889,52 @@ Node BvInverter::getInversionSkolemFor( Node cond, TypeNode tn ) {
}
}
+Node BvInverter::getInversionSkolemFunctionFor( TypeNode tn ) {
+ // function maps conditions to skolems
+ TypeNode ftn = NodeManager::currentNM()->mkFunctionType( NodeManager::currentNM()->booleanType(), tn );
+ return getSolveVariable( ftn );
+}
+
+Node BvInverter::getInversionNode( Node cond, TypeNode tn ) {
+ // condition should be rewritten
+ Node new_cond = Rewriter::rewrite(cond);
+ if( new_cond!=cond ){
+ Trace("bv-invert-debug") << "Condition " << cond << " was rewritten to " << new_cond << std::endl;
+ }
+ Node f = getInversionSkolemFunctionFor( tn );
+ return NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, new_cond );
+}
+
+bool BvInverter::isInvertible( Kind k ) {
+ // TODO : make this precise (this should correspond to all kinds that we handle in solve_bv_lit/solve_bv_constraint)
+ return k!=APPLY_UF;
+}
+
Node BvInverter::getPathToPv( Node lit, Node pv, Node sv, std::vector< unsigned >& path, std::unordered_set< TNode, TNodeHashFunction >& visited ) {
if( visited.find( lit )==visited.end() ){
visited.insert( lit );
if( lit==pv ){
return sv;
}else{
- unsigned rmod = 0; // TODO : randomize?
- for( unsigned i=0; i<lit.getNumChildren(); i++ ){
- unsigned ii = ( i + rmod )%lit.getNumChildren();
- Node litc = getPathToPv( lit[ii], pv, sv, path, visited );
- if( !litc.isNull() ){
- // path is outermost term index last
- path.push_back( ii );
- std::vector< Node > children;
- if( lit.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.push_back( lit.getOperator() );
- }
- for( unsigned j=0; j<lit.getNumChildren(); j++ ){
- children.push_back( j==ii ? litc : lit[j] );
+ // only recurse if the kind is invertible
+ // this allows us to avoid paths that go through skolem functions
+ if( isInvertible( lit.getKind() ) ){
+ unsigned rmod = 0; // TODO : randomize?
+ for( unsigned i=0; i<lit.getNumChildren(); i++ ){
+ unsigned ii = ( i + rmod )%lit.getNumChildren();
+ Node litc = getPathToPv( lit[ii], pv, sv, path, visited );
+ if( !litc.isNull() ){
+ // path is outermost term index last
+ path.push_back( ii );
+ std::vector< Node > children;
+ if( lit.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( lit.getOperator() );
+ }
+ for( unsigned j=0; j<lit.getNumChildren(); j++ ){
+ children.push_back( j==ii ? litc : lit[j] );
+ }
+ return NodeManager::currentNM()->mkNode( lit.getKind(), children );
}
- return NodeManager::currentNM()->mkNode( lit.getKind(), children );
}
}
}
@@ -883,9 +942,69 @@ Node BvInverter::getPathToPv( Node lit, Node pv, Node sv, std::vector< unsigned
return Node::null();
}
+Node BvInverter::eliminateSkolemFunctions( TNode n, std::vector< Node >& side_conditions, std::unordered_map< TNode, Node, TNodeHashFunction >& visited ) {
+ std::unordered_map< TNode, Node, TNodeHashFunction >::iterator it = visited.find( n );
+ if( it==visited.end() ){
+ Trace("bv-invert-debug") << "eliminateSkolemFunctions from " << n << "..." << std::endl;
+ Node ret = n;
+ bool childChanged = false;
+ std::vector< Node > children;
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node nc = eliminateSkolemFunctions( n[i], side_conditions, visited );
+ childChanged = childChanged || n[i]!=nc;
+ children.push_back( nc );
+ }
+ if( childChanged ){
+ ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ // now, check if it is a skolem function
+ if( ret.getKind()==APPLY_UF ){
+ Node op = ret.getOperator();
+ TypeNode tnp = op.getType();
+ // is this a skolem function?
+ std::map< TypeNode, Node >::iterator its = d_solve_var.find( tnp );
+ if( its!=d_solve_var.end() && its->second==op ){
+ Assert( ret.getNumChildren()==1 );
+ Assert( ret[0].getType().isBoolean() );
+
+ Node cond = ret[0];
+ // must rewrite now to ensure we lookup the correct skolem
+ cond = Rewriter::rewrite( cond );
+
+ // if so, we replace by the (finalized) skolem variable
+ // Notice that since we are post-rewriting, skolem functions are already eliminated from cond
+ ret = getInversionSkolemFor( cond, ret.getType() );
+
+ // also must add (substituted) side condition to vector
+ // substitute ( solve variable -> inversion skolem )
+ TNode solve_var = getSolveVariable( ret.getType() );
+ TNode tret = ret;
+ cond = cond.substitute( solve_var, tret );
+ if( std::find( side_conditions.begin(), side_conditions.end(), cond )==side_conditions.end() ){
+ side_conditions.push_back( cond );
+ }
+ }
+ }
+ Trace("bv-invert-debug") << "eliminateSkolemFunctions from " << n << " returned " << ret << std::endl;
+ visited[n] = ret;
+ return ret;
+ }else{
+ return it->second;
+ }
+}
+
+Node BvInverter::eliminateSkolemFunctions( TNode n, std::vector< Node >& side_conditions ) {
+ std::unordered_map< TNode, Node, TNodeHashFunction > visited;
+ return eliminateSkolemFunctions( n, side_conditions, visited );
+}
+
Node BvInverter::getPathToPv( Node lit, Node pv, Node sv, Node pvs, std::vector< unsigned >& path ) {
std::unordered_set< TNode, TNodeHashFunction > visited;
Node slit = getPathToPv( lit, pv, sv, path, visited );
+ // if we are able to find a (invertible) path to pv
if( !slit.isNull() ){
// substitute pvs for the other occurrences of pv
TNode tpv = pv;
@@ -929,11 +1048,9 @@ Node BvInverter::solve_bv_constraint( Node sv, Node sv_t, Node t, Kind rk, bool
// add side condition
status.d_conds.push_back (sc);
- // get the skolem variable for this side condition
- Node skv = getInversionSkolemFor (sc, solve_tn);
- // cache for substitution
- // map the skolem to its side condition
- status.d_sk_inv[ skv ] = sc;
+ // get the skolem node for this side condition
+ Node skv = getInversionNode (sc, solve_tn);
+ // now solving with the skolem node as the RHS
t = skv;
}else if( k==BITVECTOR_NEG || k==BITVECTOR_NOT ){
@@ -1022,12 +1139,15 @@ public:
};
BvInstantiator::BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){
- //FIXME : this needs to be global!! Probably move to QuantifiersEngine
- d_inverter = new BvInverter;
+ // get the global inverter utility
+ // this must be global since we need to:
+ // * process Skolem functions properly across multiple variables within the same quantifier
+ // * cache Skolem variables uniformly across multiple quantified formulas
+ d_inverter = qe->getBvInverter();
}
BvInstantiator::~BvInstantiator(){
- delete d_inverter;
+
}
void BvInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
@@ -1040,6 +1160,7 @@ void BvInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsig
void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
+ Assert( d_inverter!=NULL );
// find path to pv
std::vector< unsigned > path;
Node sv = d_inverter->getSolveVariable( pv.getType() );
@@ -1082,6 +1203,10 @@ bool BvInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, No
Trace("cegqi-bv") << " " << iti->second.size() << " candidate instantiations for " << pv << " : " << std::endl;
// the order of instantiation ids we will try
std::vector< unsigned > inst_ids_try;
+ // until we have a model-preserving selection function for BV, this must be heuristic (we only pick one literal)
+ // hence we randomize the list
+ // this helps robustness, since picking the same literal every time may be lead to a stream of value instantiations
+ std::random_shuffle( iti->second.begin(), iti->second.end() );
for( unsigned j=0; j<iti->second.size(); j++ ){
unsigned inst_id = iti->second[j];
@@ -1106,13 +1231,14 @@ bool BvInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, No
// TODO : selection criteria across multiple literals goes here
// currently, we use a naive heuristic which takes only the first solved term
- // TODO : randomize?
if( inst_ids_try.empty() ){
inst_ids_try.push_back( inst_id );
}
}
// now, try all instantiation ids we want to try
+ // typically size( inst_ids_try )=0, otherwise worst-case performance for constructing
+ // instantiations is exponential on the number of variables in this quantifier
for( unsigned j = 0; j<inst_ids_try.size(); j++ ){
unsigned inst_id = iti->second[j];
Assert( d_inst_id_to_term.find(inst_id)!=d_inst_id_to_term.end() );
@@ -1120,8 +1246,6 @@ bool BvInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, No
// try instantiation pv -> inst_term
TermProperties pv_prop_bv;
Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term << std::endl;
- // TODO : need to track dependencies between inst_term and the free variables it depends on
- // This should enforce that we do not introduce any circular dependencies when solving for further variables.
d_var_to_curr_inst_id[pv] = inst_id;
if( ci->doAddInstantiationInc( pv, inst_term, pv_prop_bv, sf, effort ) ){
return true;
@@ -1137,56 +1261,23 @@ bool BvInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, No
bool BvInstantiator::needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
// we may need to post-process the instantiation since inversion skolems need to be finalized
- return d_var_to_curr_inst_id.find(pv)!=d_var_to_curr_inst_id.end();
+ // TODO : technically skolem functions can appear in datatypes with bit-vector fields. We need to eliminate them there too.
+ return true;
}
bool BvInstantiator::postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas ) {
- Trace("cegqi-bv") << "BvInstantiator::postProcessInstantiation for " << pv << std::endl;
- // first, eliminate bound variables from all skolem conditions
- std::unordered_map< Node, unsigned, NodeHashFunction >::iterator iti = d_var_to_curr_inst_id.find( pv );
- Assert( iti!=d_var_to_curr_inst_id.end() );
- unsigned inst_id = iti->second;
- std::unordered_map< unsigned, BvInverterStatus >::iterator its = d_inst_id_to_status.find( inst_id );
- Assert( its!=d_inst_id_to_status.end() );
-
- // this maps temporary skolems (those with side conditions involving free variables) -> finalized skolems
- std::vector< Node > sk_vars_add;
- std::vector< Node > sk_subs_add;
- for( std::unordered_map< Node, Node, NodeHashFunction >::iterator itk = its->second.d_sk_inv.begin();
- itk != its->second.d_sk_inv.end(); ++itk ){
- TNode curr_skv = itk->first;
- Trace("cegqi-bv-debug") << " Skolem " << curr_skv << " has condition " << itk->second << std::endl;
- Node curr_cond = itk->second.substitute( sf.d_vars.begin(), sf.d_vars.end(), sf.d_subs.begin(), sf.d_subs.end() );
- // the condition should have no bound variables, or skolems that are associated with conditions that have bound variables.
-
- // if the condition is updated, we need to update it
- Node sk_for_curr_cond;
- if( curr_cond!=itk->second ){
- Trace("cegqi-bv-debug") << " Skolem " << curr_skv << " has condition (after substitution) " << curr_cond << std::endl;
- sk_for_curr_cond = d_inverter->getInversionSkolemFor( curr_cond, curr_skv.getType() );
- // we must replace the Skolem in the condition
- sk_vars_add.push_back( curr_skv );
- sk_subs_add.push_back( sk_for_curr_cond );
-
- // TODO : register this as a skolem that is eligible for instantiation
- }else{
- sk_for_curr_cond = curr_skv;
+ Trace("cegqi-bv") << "BvInstantiator::postProcessInstantiation " << pv << std::endl;
+ Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )!=sf.d_vars.end() );
+ unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )-sf.d_vars.begin();
+ Trace("cegqi-bv") << " postprocess : " << pv << " -> " << sf.d_subs[index] << std::endl;
+ // eliminate skolem functions from the substitution
+ unsigned prev_lem_size = lemmas.size();
+ sf.d_subs[index] = d_inverter->eliminateSkolemFunctions( sf.d_subs[index], lemmas );
+ if( Trace.isOn("cegqi-bv") ){
+ Trace("cegqi-bv") << " got : " << pv << " -> " << sf.d_subs[index] << std::endl;
+ for( unsigned i=prev_lem_size; i<lemmas.size(); i++ ){
+ Trace("cegqi-bv") << " side condition : " << lemmas[i] << std::endl;
}
-
- // we now must map the solve variable in the current condition to the final skolem
- TNode solve_var = d_inverter->getSolveVariable( sk_for_curr_cond.getType() );
- curr_cond = curr_cond.substitute( solve_var, sk_for_curr_cond );
-
- // curr_cond is now in terms of the finalized skolem
- lemmas.push_back( curr_cond );
- Trace("cegqi-bv") << " side condition : " << curr_cond << std::endl;
- }
-
- // add new substitutions
- TermProperties term_prop_skvinv;
- for( unsigned i=0; i<sk_vars_add.size(); i++ ){
- sf.push_back( sk_vars_add[i], sk_subs_add[i], term_prop_skvinv );
- Trace("cegqi-bv") << " (temporary -> final) skolem substitution : " << sk_vars_add[i] << " -> " << sk_subs_add[i] << std::endl;
}
return true;
diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index 7328df167..26f5fe62a 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -94,43 +94,85 @@ public:
BvInverterStatus() : d_status(0) {}
~BvInverterStatus(){}
int d_status;
+ // TODO : may not need this (conditions are now appear explicitly in solved forms)
// side conditions
std::vector< Node > d_conds;
- // conditions regarding the skolems in d_conds
- std::unordered_map< Node, Node, NodeHashFunction > d_sk_inv;
};
// inverter class
// TODO : move to theory/bv/ if generally useful?
class BvInverter {
private:
+ /** dummy variables for each type */
std::map< TypeNode, Node > d_solve_var;
- Node getPathToPv( Node lit, Node pv, Node sv, std::vector< unsigned >& path, std::unordered_set< TNode, TNodeHashFunction >& visited );
- // stores the inversion skolems
+ /** stores the inversion skolems, for each condition */
std::unordered_map< Node, Node, NodeHashFunction > d_inversion_skolem_cache;
+ /** helper function for getPathToPv */
+ Node getPathToPv( Node lit, Node pv, Node sv, std::vector< unsigned >& path, std::unordered_set< TNode, TNodeHashFunction >& visited );
+ /** helper function for eliminateSkolemFunctions */
+ Node eliminateSkolemFunctions( TNode n, std::vector< Node >& side_conditions, std::unordered_map< TNode, Node, TNodeHashFunction >& visited );
+ // is operator k invertible?
+ bool isInvertible( Kind k );
+ /** get inversion skolem for condition
+ * precondition : exists x. cond( x ) is a tautology in BV,
+ * where x is getSolveVariable( tn ).
+ * returns fresh skolem k of type tn, where we may assume cond( k ).
+ */
+ Node getInversionSkolemFor( Node cond, TypeNode tn );
+ /** get inversion skolem function for type tn.
+ * This is a function of type ( Bool -> tn ) that is used for explicitly storing side conditions
+ * inside terms. For all ( cond, tn ), if :
+ *
+ * f = getInversionSkolemFunctionFor( tn )
+ * k = getInversionSkolemFor( cond, tn )
+ * then:
+ * f( cond ) is a placeholder for k.
+ *
+ * In the call eliminateSkolemFunctions, we replace all f( cond ) with k and add cond{ x -> k } to side_conditions.
+ * The advantage is that f( cond ) explicitly contains the side condition so it automatically
+ * updates with substitutions.
+ */
+ Node getInversionSkolemFunctionFor( TypeNode tn );
public:
BvInverter(){}
~BvInverter(){}
- // get dummy fresh variable of type tn, used as argument for sv
+ /** get dummy fresh variable of type tn, used as argument for sv */
Node getSolveVariable( TypeNode tn );
- // get inversion skolem for condition
- // precondition : exists x. cond( x ) is a tautology in BV,
- // where x is getSolveVariable( tn ).
- // returns fresh skolem k, where we may assume cond( k ).
- Node getInversionSkolemFor( Node cond, TypeNode tn );
- // Get path to pv in lit, replace that occurrence by sv and all others by pvs.
- // e.g. if return value R is non-null, then:
- // lit.path = pv
- // R.path = sv
- // R.path' = pvs for all lit.path' = pv, where path' != path
+ /** get inversion node, if :
+ *
+ * f = getInversionSkolemFunctionFor( tn )
+ *
+ * This returns f( cond ).
+ */
+ Node getInversionNode( Node cond, TypeNode tn );
+ /** Get path to pv in lit, replace that occurrence by sv and all others by pvs.
+ * If return value R is non-null, then :
+ * lit.path = pv
+ * R.path = sv
+ * R.path' = pvs for all lit.path' = pv, where path' != path
+ */
Node getPathToPv( Node lit, Node pv, Node sv, Node pvs, std::vector< unsigned >& path );
-public:
- // solve for sv in constraint ( (pol ? _ : not) sv_t <rk> t ), where sv_t.path = sv
- // status accumulates side conditions
+ /** eliminate skolem functions in node n
+ *
+ * This eliminates all Skolem functions from Node n and replaces them with finalized
+ * Skolem variables.
+ *
+ * For each skolem variable we introduce, we ensure its associated side condition is
+ * added to side_conditions.
+ *
+ * Apart from Skolem functions, all subterms of n should be eligible for instantiation.
+ */
+ Node eliminateSkolemFunctions( TNode n, std::vector< Node >& side_conditions );
+ /** solve_bv_constraint
+ * solve for sv in constraint ( (pol ? _ : not) sv_t <rk> t ), where sv_t.path = sv
+ * status accumulates side conditions
+ */
Node solve_bv_constraint( Node sv, Node sv_t, Node t, Kind rk, bool pol, std::vector< unsigned >& path,
BvInverterModelQuery * m, BvInverterStatus& status );
- // solve for sv in lit, where lit.path = sv
- // status accumulates side conditions
+ /** solve_bv_lit
+ * solve for sv in lit, where lit.path = sv
+ * status accumulates side conditions
+ */
Node solve_bv_lit( Node sv, Node lit, bool pol, std::vector< unsigned >& path,
BvInverterModelQuery * m, BvInverterStatus& status );
};
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 34758c431..52ea7cc62 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -746,7 +746,8 @@ bool InstStrategyCegqi::addLemma( Node lem ) {
bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){
- if( n.getKind()==SKOLEM && d_quantEngine->getTermDatabase()->containsVtsTerm( n ) ){
+ if( n.getAttribute(VirtualTermSkolemAttribute()) ){
+ // virtual terms are allowed
return true;
}else{
TypeNode tn = n.getType();
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index ec5fc633d..18ba08ae2 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1656,6 +1656,9 @@ Node TermDb::getVtsDelta( bool isFree, bool create ) {
}
if( d_vts_delta.isNull() ){
d_vts_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for virtual term substitution" );
+ //mark as a virtual term
+ VirtualTermSkolemAttribute vtsa;
+ d_vts_delta.setAttribute(vtsa,true);
}
}
return isFree ? d_vts_delta_free : d_vts_delta;
@@ -1668,6 +1671,9 @@ Node TermDb::getVtsInfinity( TypeNode tn, bool isFree, bool create ) {
}
if( d_vts_inf[tn].isNull() ){
d_vts_inf[tn] = NodeManager::currentNM()->mkSkolem( "inf", tn, "infinity for virtual term substitution" );
+ //mark as a virtual term
+ VirtualTermSkolemAttribute vtsa;
+ d_vts_inf[tn].setAttribute(vtsa,true);
}
}
return isFree ? d_vts_inf_free[tn] : d_vts_inf[tn];
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 4650cc5d4..9df9da957 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -123,6 +123,9 @@ typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
struct SygusVarNumAttributeId {};
typedef expr::Attribute<SygusVarNumAttributeId, uint64_t> SygusVarNumAttribute;
+/** Attribute to mark Skolems as virtual terms */
+struct VirtualTermSkolemAttributeId {};
+typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute;
class QuantifiersEngine;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8649c7bdd..2d1ae7983 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -24,6 +24,7 @@
#include "theory/quantifiers/ambqi_builder.h"
#include "theory/quantifiers/bounded_integers.h"
#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/quantifiers/ceg_t_instantiator.h"
#include "theory/quantifiers/conjecture_generator.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/full_model_check.h"
@@ -130,6 +131,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
d_uee = NULL;
d_fs = NULL;
d_rel_dom = NULL;
+ d_bv_invert = NULL;
d_builder = NULL;
d_total_inst_count_debug = 0;
@@ -160,6 +162,7 @@ QuantifiersEngine::~QuantifiersEngine(){
delete d_qcf;
delete d_quant_rel;
delete d_rel_dom;
+ delete d_bv_invert;
delete d_model;
delete d_tr_trie;
delete d_term_db;
@@ -217,9 +220,10 @@ void QuantifiersEngine::finishInit(){
if( options::cbqi() ){
d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
d_modules.push_back( d_i_cbqi );
- //if( options::cbqiModel() ){
- // needsBuilder = true;
- //}
+ if( options::cbqiBv() ){
+ // if doing instantiation for BV, need the inverter class
+ d_bv_invert = new quantifiers::BvInverter;
+ }
}
if( options::ceGuidedInst() ){
d_ceg_inst = new quantifiers::CegInstantiation( this, c );
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 7d8f5354b..443bbd643 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -48,16 +48,20 @@ public:
};
namespace quantifiers {
+ //TODO: organize this more/review this, github issue #1163
+ //utilities
class TermDb;
class TermDbSygus;
class FirstOrderModel;
- //modules
+ class RelevantDomain;
+ class BvInverter;
+ class InstPropagator;
+ //modules, these are "subsolvers" of the quantifiers theory.
class InstantiationEngine;
class ModelEngine;
class BoundedIntegers;
class QuantConflictFind;
class RewriteEngine;
- class RelevantDomain;
class QModelBuilder;
class ConjectureGenerator;
class CegInstantiation;
@@ -71,7 +75,6 @@ namespace quantifiers {
class QuantDSplit;
class QuantAntiSkolem;
class EqualityInference;
- class InstPropagator;
}/* CVC4::theory::quantifiers */
namespace inst {
@@ -108,6 +111,8 @@ private:
QuantRelevance * d_quant_rel;
/** relevant domain */
quantifiers::RelevantDomain* d_rel_dom;
+ /** inversion utility for BV instantiation */
+ quantifiers::BvInverter * d_bv_invert;
/** alpha equivalence */
quantifiers::AlphaEquivalence * d_alpha_equiv;
/** model builder */
@@ -225,6 +230,8 @@ public:
Valuation& getValuation();
/** get relevant domain */
quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; }
+ /** get the BV inverter utility */
+ quantifiers::BvInverter * getBvInverter() { return d_bv_invert; }
/** get quantifier relevance */
QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
/** get the model builder */
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index cb6ed687e..a4bd40df5 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -89,11 +89,9 @@ TESTS = \
cbqi-sdlx-fixpoint-3-dd.smt2 \
qbv-simp.smt2 \
psyco-001-bv.smt2 \
- bug822.smt2
-
-# FIXME: solvable with --cbqi-bv
-#qbv-test-invert-mul.smt2
-#qbv-simple-2vars-vo.smt2
+ bug822.smt2 \
+ qbv-test-invert-mul.smt2 \
+ qbv-simple-2vars-vo.smt2
# regression can be solved with --finite-model-find --fmf-inst-engine
# set3.smt2
diff --git a/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2
index f38625fd8..b6ae95fec 100644
--- a/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2
+++ b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
(set-logic BV)
(set-info :status sat)
(declare-fun a () (_ BitVec 32))
@@ -6,7 +8,6 @@
(assert (not (= a #x00000000)))
-; this is sensitive to variable ordering (try changing x and y)
(assert (forall ((x (_ BitVec 32)) (y (_ BitVec 32))) (or
(not (= (bvmul x y) #x0000000A))
(not (= (bvadd y a) #x00000010))
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2
index bea19a054..235d353ef 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
(set-logic BV)
(set-info :status sat)
(declare-fun a () (_ BitVec 32))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback