diff options
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 ); }; } |