diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-04 09:19:46 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-04 09:19:46 +0100 |
| commit | 03541f4faeb820539ac25f06f1e64adc7aedca6f (patch) | |
| tree | 19e09a23a205d1598b8cba8682aadac8a1b0edee /src/theory/quantifiers/ce_guided_single_inv.h | |
| parent | 3df24b6e0480799e8f400d15778ed5d3fb2ba7ae (diff) | |
Start work on simplifying single inv solutions. Minor.
Diffstat (limited to 'src/theory/quantifiers/ce_guided_single_inv.h')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 03aaa543f..4e1578df6 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -46,6 +46,13 @@ private: bool debugSolution( Node sol ); void debugTermSize( Node sol, int& t_size, int& num_ite ); + Node pullITEs( Node n ); + bool pullITECondition( Node root, Node n, std::vector< Node >& conj, Node& t, Node& rem, int depth ); + Node simplifySolution( QuantifiersEngine * qe, Node sol, std::map< Node, bool >& assign, + std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& args, int status ); + bool getAssign( QuantifiersEngine * qe, bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign, + std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args ); + bool getAssignEquality( QuantifiersEngine * qe, Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args ); public: CegConjectureSingleInv( Node q, CegConjecture * p ); // original conjecture @@ -78,7 +85,7 @@ public: //check void check( QuantifiersEngine * qe, std::vector< Node >& lems ); //get solution - Node getSolution( unsigned i, Node varList ); + Node getSolution( QuantifiersEngine * qe, unsigned i, Node varList ); }; } |