diff options
Diffstat (limited to 'src/theory/quantifiers/bv_inverter.h')
-rw-r--r-- | src/theory/quantifiers/bv_inverter.h | 62 |
1 files changed, 28 insertions, 34 deletions
diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index a44d64904..ce2a58695 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -44,47 +44,22 @@ class BvInverterQuery virtual Node getBoundVariable(TypeNode tn) = 0; }; -// class for storing information about the solved status -class BvInverterStatus { - public: - BvInverterStatus() : d_status(0) {} - ~BvInverterStatus() {} - int d_status; -}; - // inverter class // TODO : move to theory/bv/ if generally useful? -class BvInverter { +class BvInverter +{ public: BvInverter() {} ~BvInverter() {} /** get dummy fresh variable of type tn, used as argument for sv */ Node getSolveVariable(TypeNode tn); - /** get inversion node - * - * This expects a condition cond where: - * (exists x. cond) - * is a BV tautology where x is getSolveVariable( tn ). - * - * It returns a term of the form: - * (choice y. cond { x -> y }) - * where y is a bound variable and x is getSolveVariable( tn ). - * - * In some cases, we may return a term t - * if cond implies an equality on the solve variable. - * For example, if cond is x = t where x is - * getSolveVariable( tn ), then we return t - * instead of introducing the choice function. - */ - Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m); - /** 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); + Node getPathToPv( + Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path); /** solveBvLit * solve for sv in lit, where lit.path = sv @@ -93,16 +68,35 @@ class BvInverter { Node solveBvLit(Node sv, Node lit, std::vector<unsigned>& path, - BvInverterQuery* m, - BvInverterStatus& status); + BvInverterQuery* m); private: - /** dummy variables for each type */ + /** Dummy variables for each type */ std::map<TypeNode, Node> d_solve_var; - /** helper function for getPathToPv */ - Node getPathToPv(Node lit, Node pv, Node sv, std::vector<unsigned>& path, + /** 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 getInv. + * + * This expects a condition cond where: + * (exists x. cond) + * is a BV tautology where x is getSolveVariable( tn ). + * + * It returns a term of the form: + * (choice y. cond { x -> y }) + * where y is a bound variable and x is getSolveVariable( tn ). + * + * In some cases, we may return a term t if cond implies an equality on + * the solve variable. For example, if cond is x = t where x is + * getSolveVariable(tn), then we return t instead of introducing the choice + * function. + */ + Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m); }; } // namespace quantifiers |