diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-27 17:27:57 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-27 17:27:57 +0200 |
commit | 0ddf1b9c74f2b2a78e0960b710c2edbdc5f8d02d (patch) | |
tree | 523a7c7ec9bfefd4297c5d8f56ef0ff474045d73 /src/theory/quantifiers/inst_strategy_cbqi.h | |
parent | d4a7b0cf0500e971c9c01e7628f3c1b567715059 (diff) |
Do ITE term bookkeeping when solving Sygus inputs. Add missing script from Sygus comp 2015. Fix bug 665 regarding strings rewriter for contains.
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.h')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 0056671be..f882da110 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -9,14 +9,14 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief instantiator_arith_instantiator + ** \brief counterexample-guided quantifier instantiation **/ #include "cvc4_private.h" -#ifndef __CVC4__INST_STRATEGT_CBQI_H -#define __CVC4__INST_STRATEGT_CBQI_H +#ifndef __CVC4__INST_STRATEGY_CBQI_H +#define __CVC4__INST_STRATEGY_CBQI_H #include "theory/quantifiers/instantiation_engine.h" #include "theory/arith/arithvar.h" @@ -30,10 +30,6 @@ namespace arith { class TheoryArith; } -namespace datatypes { - class TheoryDatatypes; -} - namespace quantifiers { class CegqiOutput @@ -64,6 +60,12 @@ private: std::map< Node, std::vector< Node > > d_curr_eqc; std::map< Node, Node > d_curr_rep; std::vector< Node > d_curr_arith_eqc; + //auxiliary variables + std::vector< Node > d_aux_vars; + //literals to equalities for aux vars + std::map< Node, std::map< Node, Node > > d_aux_eq; + //the CE variables + std::vector< Node > d_vars; private: //for adding instantiations during check void computeProgVars( Node n ); @@ -87,16 +89,12 @@ private: void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); public: CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); - //the CE variables - std::vector< Node > d_vars; - //auxiliary variables - std::vector< Node > d_aux_vars; - //literals to equalities for aux vars - std::map< Node, std::map< Node, Node > > d_aux_eq; //check : add instantiations based on valuation of d_vars bool check(); //presolve for quantified formula void presolve( Node q ); + //register the counterexample lemma (stored in lems), modify vector + void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ); }; class InstStrategySimplex : public InstStrategy{ |