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 \
--- /dev/null
+/********************* */
+/*! \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();
+}
--- /dev/null
+/********************* */
+/*! \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 */
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 ){}
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:
return true;
}
-
-
#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>
};
-// 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
projects / cvc5.git / commitdiff