From: Andrew Reynolds Date: Fri, 29 Sep 2017 19:28:52 +0000 (-0500) Subject: Simplify representation of inversion Skolems for bv cegqi (#1164) X-Git-Tag: cvc5-1.0.0~5597 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b48120e1c224208eaef28f86e77830f211852f9b;p=cvc5.git Simplify representation of inversion Skolems for bv cegqi (#1164) * Simplify intermediate representation of inversion skolems for cegqi bit-vectors. Cache bv inversion status globally in QuantifierEngine. Generalize virtual term policy for marking eligible instantiation terms. Enable regression. * Enable other regression --- 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 + 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 children; - if( lit.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( lit.getOperator() ); - } - for( unsigned j=0; j children; + if( lit.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( lit.getOperator() ); + } + for( unsigned j=0; jmkNode( 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; imkNode( 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; jsecond.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; jsecond[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; igetSolveVariable( 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 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 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 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 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))