diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile.am | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 347 | ||||
| -rw-r--r-- | src/theory/quantifiers/bv_inverter.h | 150 | ||||
| -rw-r--r-- | src/theory/quantifiers/ceg_t_instantiator.cpp | 299 | ||||
| -rw-r--r-- | src/theory/quantifiers/ceg_t_instantiator.h | 98 |
5 files changed, 504 insertions, 392 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index da8558527..3a41b30ab 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -346,6 +346,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/anti_skolem.h \ theory/quantifiers/bounded_integers.cpp \ theory/quantifiers/bounded_integers.h \ + theory/quantifiers/bv_inverter.cpp \ + theory/quantifiers/bv_inverter.h \ theory/quantifiers/candidate_generator.cpp \ theory/quantifiers/candidate_generator.h \ theory/quantifiers/ce_guided_instantiation.cpp \ diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp new file mode 100644 index 000000000..a0b78d6d4 --- /dev/null +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -0,0 +1,347 @@ +/********************* */ +/*! \file bv_inverter.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief inverse rules for bit-vector operators + **/ + +#include "theory/quantifiers/bv_inverter.h" + +#include <algorithm> + +#include "theory/quantifiers/term_database.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::theory::quantifiers; + +Node BvInverter::getSolveVariable(TypeNode tn) { + std::map<TypeNode, Node>::iterator its = d_solve_var.find(tn); + if (its == d_solve_var.end()) { + 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 { + return its->second; + } +} + +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; + 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 { + Assert(it->second.getType() == tn); + return it->second; + } +} + +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 { + // 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 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; + TNode tpvs = pvs; + slit = slit.substitute(tpv, tpvs); + } + return slit; +} + +Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk, + bool pol, std::vector<unsigned>& path, + BvInverterModelQuery* m, + BvInverterStatus& status) { + NodeManager* nm = NodeManager::currentNM(); + while (!path.empty()) { + unsigned index = path.back(); + Assert(sv_t.getNumChildren() <= 2); + Assert(index < sv_t.getNumChildren()); + path.pop_back(); + Kind k = sv_t.getKind(); + // inversions + if (k == BITVECTOR_PLUS) { + t = nm->mkNode(BITVECTOR_SUB, t, sv_t[1 - index]); + } else if (k == BITVECTOR_SUB) { + t = nm->mkNode(BITVECTOR_PLUS, t, sv_t[1 - index]); + } else if (k == BITVECTOR_MULT) { + // t = skv (fresh skolem constant) + TypeNode solve_tn = sv_t[index].getType(); + Node x = getSolveVariable(solve_tn); + // with side condition: + // ctz(t) >= ctz(s) <-> x * s = t + // where + // ctz(t) >= ctz(s) -> (t & -t) >= (s & -s) + Node s = sv_t[1 - index]; + // left hand side of side condition + Node scl = nm->mkNode( + BITVECTOR_UGE, + nm->mkNode(BITVECTOR_AND, t, nm->mkNode(BITVECTOR_NEG, t)), + nm->mkNode(BITVECTOR_AND, s, nm->mkNode(BITVECTOR_NEG, s))); + // right hand side of side condition + Node scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_MULT, x, s), t); + // overall side condition + Node sc = nm->mkNode(IMPLIES, scl, scr); + // add side condition + status.d_conds.push_back(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) { + t = NodeManager::currentNM()->mkNode(k, t); + //}else if( k==BITVECTOR_AND || k==BITVECTOR_OR ){ + // TODO + //}else if( k==BITVECTOR_CONCAT ){ + // TODO + //}else if( k==BITVECTOR_SHL || k==BITVECTOR_LSHR ){ + // TODO + //}else if( k==BITVECTOR_ASHR ){ + // TODO + } else { + Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector term " << k + << ", from " << sv_t << std::endl; + return Node::null(); + } + sv_t = sv_t[index]; + } + Assert(sv_t == sv); + // finalize based on the kind of constraint + // TODO + if (rk == EQUAL) { + return t; + } else { + Trace("bv-invert") + << "bv-invert : Unknown relation kind for bit-vector literal " << rk + << std::endl; + return t; + } +} + +Node BvInverter::solve_bv_lit(Node sv, Node lit, bool pol, + std::vector<unsigned>& path, + BvInverterModelQuery* m, + BvInverterStatus& status) { + Assert(!path.empty()); + unsigned index = path.back(); + Assert(index < lit.getNumChildren()); + path.pop_back(); + Kind k = lit.getKind(); + if (k == NOT) { + Assert(index == 0); + return solve_bv_lit(sv, lit[index], !pol, path, m, status); + } else if (k == EQUAL) { + return solve_bv_constraint(sv, lit[index], lit[1 - index], k, pol, path, m, + status); + } else if (k == BITVECTOR_ULT || k == BITVECTOR_ULE || k == BITVECTOR_SLT || + k == BITVECTOR_SLE) { + if (!pol) { + if (k == BITVECTOR_ULT) { + k = index == 1 ? BITVECTOR_ULE : BITVECTOR_UGE; + } else if (k == BITVECTOR_ULE) { + k = index == 1 ? BITVECTOR_ULT : BITVECTOR_UGT; + } else if (k == BITVECTOR_SLT) { + k = index == 1 ? BITVECTOR_SLE : BITVECTOR_SGE; + } else { + Assert(k == BITVECTOR_SLE); + k = index == 1 ? BITVECTOR_SLT : BITVECTOR_SGT; + } + } else if (index == 1) { + if (k == BITVECTOR_ULT) { + k = BITVECTOR_UGT; + } else if (k == BITVECTOR_ULE) { + k = BITVECTOR_UGE; + } else if (k == BITVECTOR_SLT) { + k = BITVECTOR_SGT; + } else { + Assert(k == BITVECTOR_SLE); + k = BITVECTOR_SGE; + } + } + return solve_bv_constraint(sv, lit[index], lit[1 - index], k, true, path, m, + status); + } else { + Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector literal " + << lit << std::endl; + } + return Node::null(); +} diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h new file mode 100644 index 000000000..ca6c97f83 --- /dev/null +++ b/src/theory/quantifiers/bv_inverter.h @@ -0,0 +1,150 @@ +/********************* */ +/*! \file bv_inverter.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief inverse rules for bit-vector operators + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BV_INVERTER_H +#define __CVC4__BV_INVERTER_H + +#include <map> +#include <unordered_map> +#include <unordered_set> +#include <vector> + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +// virtual class for model queries +class BvInverterModelQuery { + public: + BvInverterModelQuery() {} + ~BvInverterModelQuery() {} + virtual Node getModelValue(Node n) = 0; +}; + +// class for storing information about the solved status +class BvInverterStatus { + 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; +}; + +// inverter class +// TODO : move to theory/bv/ if generally useful? +class BvInverter { + public: + BvInverter() {} + ~BvInverter() {} + + /** get dummy fresh variable of type tn, used as argument for sv */ + Node getSolveVariable(TypeNode tn); + + /** 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); + + /** 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_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); + + private: + /** dummy variables for each type */ + std::map<TypeNode, Node> d_solve_var; + + /** 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); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__BV_INVERTER_H */ diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index e2065ffd9..498d618d1 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -833,301 +833,8 @@ bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, N return false; } -Node BvInverter::getSolveVariable( TypeNode tn ) { - std::map< TypeNode, Node >::iterator its = d_solve_var.find( tn ); - if( its==d_solve_var.end() ){ - 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{ - return its->second; - } -} - -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; - 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{ - Assert( it->second.getType()==tn ); - return it->second; - } -} - -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{ - // 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 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; - TNode tpvs = pvs; - slit = slit.substitute( tpv, tpvs ); - } - return slit; -} - -Node BvInverter::solve_bv_constraint( Node sv, Node sv_t, Node t, Kind rk, bool pol, std::vector< unsigned >& path, - BvInverterModelQuery * m, BvInverterStatus& status ) { - NodeManager *nm = NodeManager::currentNM(); - while( !path.empty() ){ - unsigned index = path.back(); - Assert (sv_t.getNumChildren() <= 2); - Assert( index<sv_t.getNumChildren() ); - path.pop_back(); - Kind k = sv_t.getKind(); - // inversions - if( k==BITVECTOR_PLUS ){ - t = nm->mkNode( BITVECTOR_SUB, t, sv_t[1-index] ); - }else if( k==BITVECTOR_SUB ){ - t = nm->mkNode( BITVECTOR_PLUS, t, sv_t[1-index] ); - }else if( k==BITVECTOR_MULT ){ - // t = skv (fresh skolem constant) - TypeNode solve_tn = sv_t[index].getType(); - Node x = getSolveVariable( solve_tn ); - // with side condition: - // ctz(t) >= ctz(s) <-> x * s = t - // where - // ctz(t) >= ctz(s) -> (t & -t) >= (s & -s) - Node s = sv_t[1-index]; - // left hand side of side condition - Node scl = nm->mkNode (BITVECTOR_UGE, - nm->mkNode (BITVECTOR_AND, t, nm->mkNode (BITVECTOR_NEG, t)), - nm->mkNode (BITVECTOR_AND, s, nm->mkNode (BITVECTOR_NEG, s))); - // right hand side of side condition - Node scr = nm->mkNode (EQUAL, nm->mkNode (BITVECTOR_MULT, x, s), t); - // overall side condition - Node sc = nm->mkNode (IMPLIES, scl, scr); - // add side condition - status.d_conds.push_back (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 ){ - t = NodeManager::currentNM()->mkNode( k, t ); - //}else if( k==BITVECTOR_AND || k==BITVECTOR_OR ){ - // TODO - //}else if( k==BITVECTOR_CONCAT ){ - // TODO - //}else if( k==BITVECTOR_SHL || k==BITVECTOR_LSHR ){ - // TODO - //}else if( k==BITVECTOR_ASHR ){ - // TODO - }else{ - Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector term " << k << ", from " << sv_t << std::endl; - return Node::null(); - } - sv_t = sv_t[index]; - } - Assert( sv_t==sv ); - // finalize based on the kind of constraint - //TODO - if( rk==EQUAL ){ - return t; - }else{ - Trace("bv-invert") << "bv-invert : Unknown relation kind for bit-vector literal " << rk << std::endl; - return t; - } -} - -Node BvInverter::solve_bv_lit( Node sv, Node lit, bool pol, std::vector< unsigned >& path, - BvInverterModelQuery * m, BvInverterStatus& status ){ - Assert( !path.empty() ); - unsigned index = path.back(); - Assert( index<lit.getNumChildren() ); - path.pop_back(); - Kind k = lit.getKind(); - if( k==NOT ){ - Assert( index==0 ); - return solve_bv_lit( sv, lit[index], !pol, path, m, status ); - }else if( k==EQUAL ){ - return solve_bv_constraint( sv, lit[index], lit[1-index], k, pol, path, m, status ); - }else if( k==BITVECTOR_ULT || k==BITVECTOR_ULE || k==BITVECTOR_SLT || k==BITVECTOR_SLE ){ - if( !pol ){ - if( k==BITVECTOR_ULT ){ - k = index==1 ? BITVECTOR_ULE : BITVECTOR_UGE; - }else if( k==BITVECTOR_ULE ){ - k = index==1 ? BITVECTOR_ULT : BITVECTOR_UGT; - }else if( k==BITVECTOR_SLT ){ - k = index==1 ? BITVECTOR_SLE : BITVECTOR_SGE; - }else{ - Assert( k==BITVECTOR_SLE ); - k = index==1 ? BITVECTOR_SLT : BITVECTOR_SGT; - } - }else if( index==1 ){ - if( k==BITVECTOR_ULT ){ - k = BITVECTOR_UGT; - }else if( k==BITVECTOR_ULE ){ - k = BITVECTOR_UGE; - }else if( k==BITVECTOR_SLT ){ - k = BITVECTOR_SGT; - }else{ - Assert( k==BITVECTOR_SLE ); - k = BITVECTOR_SGE; - } - } - return solve_bv_constraint( sv, lit[index], lit[1-index], k, true, path, m, status ); - }else{ - Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector literal " << lit << std::endl; - } - return Node::null(); -} - // this class can be used to query the model value through the CegInstaniator class class CegInstantiatorBvInverterModelQuery : public BvInverterModelQuery { -protected: - // pointer to class that is able to query model values - CegInstantiator * d_ci; public: CegInstantiatorBvInverterModelQuery( CegInstantiator * ci ) : BvInverterModelQuery(), d_ci( ci ){} @@ -1136,8 +843,12 @@ public: Node getModelValue( Node n ) { return d_ci->getModelValue( n ); } +protected: + // pointer to class that is able to query model values + CegInstantiator * d_ci; }; + BvInstantiator::BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){ // get the global inverter utility // this must be global since we need to: @@ -1282,5 +993,3 @@ bool BvInstantiator::postProcessInstantiationForVariable( CegInstantiator * ci, return true; } - - diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h index 26f5fe62a..fff608b82 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -18,6 +18,7 @@ #ifndef __CVC4__CEG_T_INSTANTIATOR_H #define __CVC4__CEG_T_INSTANTIATOR_H +#include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/ceg_instantiator.h" #include <unordered_set> @@ -80,103 +81,6 @@ public: }; -// virtual class for model queries -class BvInverterModelQuery { -public: - BvInverterModelQuery(){} - ~BvInverterModelQuery(){} - virtual Node getModelValue( Node n ) = 0; -}; - -// class for storing information about the solved status -class BvInverterStatus { -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; -}; - -// 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; - /** 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 */ - Node getSolveVariable( TypeNode tn ); - /** 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 ); - /** 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_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 ); -}; - class BvInstantiator : public Instantiator { private: // point to the bv inverter class |