diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 13:35:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 13:35:07 -0500 |
commit | 13e452be03bef09e2f54f42e2bc42383505ffcea (patch) | |
tree | 39695fe22d387bc84bc49d20831a19648d55011f /src/theory/quantifiers/bv_inverter.h | |
parent | be11fae39055f213586058ec9129d1276f724b0e (diff) |
CBQI BV choice expressions (#1296)
* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently.
* Minor
* Make unique bound variables for choice functions in BvInstantor, clean up.
* Incorporate missing optimizations
* Clang format
* Unused field.
* Minor
* Fix, add regression.
* Fix regression.
* Fix bug that led to incorrect cleanup of instantiations.
* Add missing regression
* Improve handling of choice rewriting.
* Fix
* Clang format
* Use canonical variables for choice functions in cbqi bv.
* Add regression
* Clang format.
* Address review.
* Clang format
Diffstat (limited to 'src/theory/quantifiers/bv_inverter.h')
-rw-r--r-- | src/theory/quantifiers/bv_inverter.h | 81 |
1 files changed, 31 insertions, 50 deletions
diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index 1c60d11ea..56f8d492b 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -28,12 +28,20 @@ namespace CVC4 { namespace theory { namespace quantifiers { -// virtual class for model queries -class BvInverterModelQuery { +/** BvInverterQuery + * + * This is a virtual class for queries + * required by the BvInverter class. + */ +class BvInverterQuery +{ public: - BvInverterModelQuery() {} - ~BvInverterModelQuery() {} + BvInverterQuery() {} + ~BvInverterQuery() {} + /** returns the current model value of n */ virtual Node getModelValue(Node n) = 0; + /** returns a bound variable of type tn */ + virtual Node getBoundVariable(TypeNode tn) = 0; }; // class for storing information about the solved status @@ -53,17 +61,26 @@ 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 : + /** get inversion node + * + * This expects a condition cond where: + * (exists x. cond) + * is a BV tautology where x is getSolveVariable( tn ). * - * f = getInversionSkolemFunctionFor( tn ) + * It returns a term of the form: + * (choice y. cond { x -> y }) + * where y is a bound variable and x is getSolveVariable( tn ). * - * This returns f( cond ). + * 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); + 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 @@ -72,62 +89,26 @@ class BvInverter { 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_lit * solve for sv in lit, where lit.path = sv * status accumulates side conditions */ - Node solve_bv_lit(Node sv, Node lit, std::vector<unsigned>& path, - BvInverterModelQuery* m, BvInverterStatus& status); + Node solve_bv_lit(Node sv, + Node lit, + std::vector<unsigned>& path, + BvInverterQuery* 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); // is operator k invertible? bool isInvertible(Kind k, unsigned index); - - /** 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 |