* Initial support for solving bit-vector inequalities in cegqi-bv using conversion to positive equality + model value slack.
* Clang format, remove heuristic.
* Update regressions.
* Simplify interface for CegInstantiator
//[4] directly look at assertions
if( vinst->hasProcessAssertion( this, sf, pv, effort ) ){
Trace("cbqi-inst-debug") << "[4] try based on assertions." << std::endl;
- std::vector< Node > lits;
+ std::unordered_set< Node, NodeHashFunction > lits;
//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;
if( ita!=d_curr_asserts.end() ){
for (unsigned j = 0; j<ita->second.size(); j++) {
Node lit = ita->second[j];
- if( std::find( lits.begin(), lits.end(), lit )==lits.end() ){
- lits.push_back( lit );
- if( vinst->hasProcessAssertion( this, sf, pv, lit, effort ) ){
- Trace("cbqi-inst-debug2") << " look at " << lit << std::endl;
+ if( lits.find(lit)==lits.end() ){
+ lits.insert(lit);
+ Node plit =
+ vinst->hasProcessAssertion(this, sf, pv, lit, effort);
+ if (!plit.isNull()) {
+ Trace("cbqi-inst-debug2") << " look at " << lit;
+ if (plit != lit) {
+ Trace("cbqi-inst-debug2") << "...processed to : " << plit;
+ }
+ Trace("cbqi-inst-debug2") << std::endl;
// apply substitutions
- Node slit = applySubstitutionToLiteral( lit, sf );
+ Node slit = applySubstitutionToLiteral(plit, sf);
if( !slit.isNull() ){
Trace("cbqi-inst-debug") << "...try based on literal " << slit << std::endl;
// check if contains pv
if( hasVariable( slit, pv ) ){
- if( vinst->processAssertion( this, sf, pv, slit, effort ) ){
- return true;
+ if (vinst->processAssertion(this, sf, pv, slit, lit,
+ effort)) {
+ return true;
}
}
}
}
}
}
- if( vinst->processAssertions( this, sf, pv, lits, effort ) ){
+ if (vinst->processAssertions(this, sf, pv, effort)) {
return true;
}
}
// whether the instantiator implements processAssertion for any literal
virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
- // whether the instantiator implements processAssertion for literal lit
- virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; }
- // Called when the entailment:
- // E |= lit
- // holds in current context E. Typically, lit belongs to the list of current assertions.
- // Returns true if an instantiation was successfully added via a recursive call
- virtual bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; }
- // Called after processAssertion is called for each literal asserted to the instantiator.
- virtual bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { return false; }
+ /** has process assertion
+ *
+ * Called when the entailment:
+ * E |= lit
+ * holds in current context E. Typically, lit belongs to the list of current
+ * assertions.
+ *
+ * This function is used to determine whether the instantiator implements
+ * processAssertion for literal lit.
+ * If this function returns null, then this intantiator does not handle the
+ * literal lit
+ * Otherwise, this function returns a literal lit' with the properties:
+ * (1) lit' is true in the current model,
+ * (2) lit' implies lit.
+ * where typically lit' = lit.
+ */
+ virtual Node hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv,
+ Node lit, unsigned effort) {
+ return Node::null();
+ }
+ /** process assertion
+ * Processes the assertion slit for variable pv
+ *
+ * lit is the substituted form (under sf) of a literal returned by
+ * hasProcessAssertion
+ * alit is the asserted literal, given as input to hasProcessAssertion
+ *
+ * Returns true if an instantiation was successfully added via a recursive call
+ */
+ virtual bool processAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv,
+ Node lit, Node alit, unsigned effort) {
+ return false;
+ }
+ /** process assertions
+ * Called after processAssertion is called for each literal asserted to the
+ * instantiator.
+ */
+ virtual bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv,
+ unsigned effort) {
+ return false;
+ }
//do we use the model value as instantiation for pv
virtual bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
return false;
}
-bool ArithInstantiator::hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
+Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf,
+ Node pv, Node lit,
+ unsigned effort) {
Node atom = lit.getKind()==NOT ? lit[0] : lit;
bool pol = lit.getKind()!=NOT;
//arithmetic inequalities and disequalities
- return atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() );
+ if (atom.getKind() == GEQ ||
+ (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal())) {
+ return lit;
+ } else {
+ return Node::null();
+ }
}
-bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
+bool ArithInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf,
+ Node pv, Node lit, Node alit,
+ unsigned effort) {
Node atom = lit.getKind()==NOT ? lit[0] : lit;
bool pol = lit.getKind()!=NOT;
//arithmetic inequalities and disequalities
return false;
}
-bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) {
- if( options::cbqiModel() ){
+bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
+ Node pv, unsigned effort) {
+ if (options::cbqiModel()) {
bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() );
bool upper_first = false;
if( options::cbqiMinBounds() ){
d_var_to_inst_id.clear();
d_inst_id_to_term.clear();
d_inst_id_to_status.clear();
+ d_inst_id_to_alit.clear();
d_var_to_curr_inst_id.clear();
+ d_alit_to_model_slack.clear();
}
-
-void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
+void BvInstantiator::processLiteral(CegInstantiator* ci, SolvedForm& sf,
+ Node pv, Node lit, Node alit,
+ unsigned effort) {
Assert( d_inverter!=NULL );
// find path to pv
std::vector< unsigned > path;
// store information for id and increment
d_var_to_inst_id[pv].push_back( iid );
d_inst_id_to_term[iid] = inst;
+ d_inst_id_to_alit[iid] = alit;
d_inst_id_counter++;
}else{
// cleanup information if we failed to solve
}
}
-bool BvInstantiator::hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
- return true;
+Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf,
+ Node pv, Node lit, unsigned effort) {
+ Node atom = lit.getKind() == NOT ? lit[0] : lit;
+ bool pol = lit.getKind() != NOT;
+ Kind k = atom.getKind();
+ if (pol && k == EQUAL) {
+ // positively asserted equalities between bitvector terms we leave unmodifed
+ if (atom[0].getType().isBitVector()) {
+ return lit;
+ }
+ } else {
+ // for all other predicates, we convert them to a positive equality based on
+ // the current model M, e.g.:
+ // (not) s ~ t ---> s = t + ( s^M - t^M )
+ if (k == EQUAL || k == BITVECTOR_ULT || k == BITVECTOR_ULE ||
+ k == BITVECTOR_SLT || k == BITVECTOR_SLE) {
+ Node s = atom[0];
+ Node t = atom[1];
+ // only handle equalities between bitvectors
+ if (s.getType().isBitVector()) {
+ NodeManager* nm = NodeManager::currentNM();
+ Node sm = ci->getModelValue(s);
+ Assert(!sm.isNull() && sm.isConst());
+ Node tm = ci->getModelValue(t);
+ Assert(!tm.isNull() && tm.isConst());
+ if (sm != tm) {
+ Node slack =
+ Rewriter::rewrite(nm->mkNode(kind::BITVECTOR_SUB, sm, tm));
+ Assert(slack.isConst());
+ // remember the slack value for the asserted literal
+ d_alit_to_model_slack[lit] = slack;
+ Node ret = nm->mkNode(kind::EQUAL, s,
+ nm->mkNode(kind::BITVECTOR_PLUS, t, slack));
+ Trace("cegqi-bv") << "Process " << lit << " as " << ret
+ << ", slack is " << slack << std::endl;
+ return ret;
+ }
+ }
+ }
+ }
+ return Node::null();
}
-bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
+bool BvInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf,
+ Node pv, Node lit, Node alit,
+ unsigned effort) {
// if option enabled, use approach for word-level inversion for BV instantiation
if( options::cbqiBv() ){
// get the best rewritten form of lit for solving for pv
Trace("cegqi-bv") << "...rewritten to " << rlit << std::endl;
}
}
- processLiteral( ci, sf, pv, rlit, effort );
+ processLiteral(ci, sf, pv, rlit, alit, effort);
}
return false;
}
-bool BvInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) {
+bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
+ Node pv, unsigned effort) {
std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction >::iterator iti = d_var_to_inst_id.find( pv );
if( iti!=d_var_to_inst_id.end() ){
Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl;
// 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];
Assert( d_inst_id_to_term.find(inst_id)!=d_inst_id_to_term.end() );
Node inst_term = d_inst_id_to_term[inst_id];
+ Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end());
+ Node alit = d_inst_id_to_alit[inst_id];
+
+ // get the slack value introduced for the asserted literal
+ Node curr_slack_val;
+ std::unordered_map<Node, Node, NodeHashFunction>::iterator itms =
+ d_alit_to_model_slack.find(alit);
+ if (itms != d_alit_to_model_slack.end()) {
+ curr_slack_val = itms->second;
+ }
+
// debug printing
if( Trace.isOn("cegqi-bv") ){
Trace("cegqi-bv") << " [" << j << "] : ";
Trace("cegqi-bv") << inst_term << std::endl;
+ if (!curr_slack_val.isNull()) {
+ Trace("cegqi-bv") << " ...with slack value : " << curr_slack_val
+ << std::endl;
+ }
// process information about solved status
std::unordered_map< unsigned, BvInverterStatus >::iterator its = d_inst_id_to_status.find( inst_id );
Assert( its!=d_inst_id_to_status.end() );
}
Trace("cegqi-bv") << std::endl;
}
- // TODO : selection criteria across multiple literals goes here
-
- // currently, we use a naive heuristic which takes only the first solved term
+
+ // currently we take select the first literal
if( inst_ids_try.empty() ){
+ // try the first one
inst_ids_try.push_back( inst_id );
+ } else {
+ // selection criteria across multiple literals goes here
+
+
}
}
bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort );
bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
- bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
- bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
- bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort );
+ Node hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv,
+ Node lit, unsigned effort);
+ bool processAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit,
+ Node alit, unsigned effort);
+ bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv,
+ unsigned effort);
bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas );
std::string identify() const { return "Arith"; }
// point to the bv inverter class
BvInverter * d_inverter;
unsigned d_inst_id_counter;
+ /** information about solved forms */
std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction > d_var_to_inst_id;
std::unordered_map< unsigned, Node > d_inst_id_to_term;
std::unordered_map< unsigned, BvInverterStatus > d_inst_id_to_status;
+ std::unordered_map<unsigned, Node> d_inst_id_to_alit;
// variable to current id we are processing
std::unordered_map< Node, unsigned, NodeHashFunction > d_var_to_curr_inst_id;
+ /** the amount of slack we added for asserted literals */
+ std::unordered_map<Node, Node, NodeHashFunction> d_alit_to_model_slack;
/** rewrite assertion for solve pv
* returns a literal that is equivalent to lit that leads to best solved form for pv
*/
Node rewriteAssertionForSolvePv( Node pv, Node lit );
-private:
- void processLiteral( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
-public:
+ /** process literal, called from processAssertion
+ * lit is the literal to solve for pv that has been rewritten according to
+ * internal rules here.
+ * alit is the asserted literal that lit is derived from.
+ */
+ void processLiteral(CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit,
+ Node alit, unsigned effort);
+
+ public:
BvInstantiator( QuantifiersEngine * qe, TypeNode tn );
virtual ~BvInstantiator();
void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
- bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
- bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
- bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort );
+ Node hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv,
+ Node lit, unsigned effort);
+ bool processAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit,
+ Node alit, unsigned effort);
+ bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv,
+ unsigned effort);
bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas );
bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
qbv-test-invert-bvor.smt2 \
qbv-test-invert-bvlshr-0.smt2 \
qbv-test-invert-bvurem-1.smt2 \
- qbv-simple-2vars-vo.smt2 \
qbv-test-invert-concat-0.smt2 \
qbv-test-invert-concat-1.smt2 \
qbv-test-invert-shl.smt2 \
qbv-test-invert-udiv-0.smt2 \
qbv-test-invert-udiv-1.smt2 \
- qbv-test-urem-rewrite.smt2
+ qbv-simple-2vars-vo.smt2 \
+ qbv-test-urem-rewrite.smt2 \
+ qbv-inequality2.smt2 \
+ qbv-test-invert-bvult-1.smt2
+
# regression can be solved with --finite-model-find --fmf-inst-engine
# set3.smt2
--- /dev/null
+; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 32))
+(declare-fun b () (_ BitVec 32))
+
+
+(assert (forall ((x (_ BitVec 32))) (or (bvuge x (bvadd a b)) (bvule x b))))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 3))
+(declare-fun b () (_ BitVec 3))
+(declare-fun c () (_ BitVec 3))
+
+(assert (forall ((x (_ BitVec 3))) (or (not (= (bvmul x a) b)) (bvuge x c))))
+
+(check-sat)
projects / cvc5.git / commitdiff