diff options
Diffstat (limited to 'src/theory/quantifiers/ceg_instantiator.h')
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.h | 135 |
1 files changed, 135 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h new file mode 100644 index 000000000..7dd6ef12b --- /dev/null +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -0,0 +1,135 @@ +/********************* */ +/*! \file ceg_instantiator.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief counterexample-guided quantifier instantiation + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__CEG_INSTANTIATOR_H +#define __CVC4__CEG_INSTANTIATOR_H + +#include "theory/quantifiers_engine.h" +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace theory { + +namespace arith { + class TheoryArith; +} + +namespace quantifiers { + +class CegqiOutput { +public: + virtual ~CegqiOutput() {} + virtual bool addInstantiation( std::vector< Node >& subs ) = 0; + virtual bool isEligibleForInstantiation( Node n ) = 0; + virtual bool addLemma( Node lem ) = 0; +}; + +class CegInstantiator { +private: + QuantifiersEngine * d_qe; + CegqiOutput * d_out; + //constants + Node d_zero; + Node d_one; + Node d_true; + bool d_use_vts_delta; + bool d_use_vts_inf; + //program variable contains cache + std::map< Node, std::map< Node, bool > > d_prog_var; + std::map< Node, bool > d_inelig; + //current assertions + std::map< TheoryId, std::vector< Node > > d_curr_asserts; + std::map< Node, std::vector< Node > > d_curr_eqc; + std::map< TypeNode, std::vector< Node > > d_curr_type_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; + //atoms of the CE lemma + bool d_is_nested_quant; + std::vector< Node > d_ce_atoms; +private: + //collect atoms + void collectCeAtoms( Node n, std::map< Node, bool >& visited ); + //for adding instantiations during check + void computeProgVars( Node n ); + //solved form, involves substitution with coefficients + class SolvedForm { + public: + std::vector< Node > d_subs; + std::vector< Node > d_coeff; + std::vector< Node > d_has_coeff; + void copy( SolvedForm& sf ){ + d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() ); + d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() ); + d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() ); + } + void push_back( Node pv, Node n, Node pv_coeff ){ + d_subs.push_back( n ); + d_coeff.push_back( pv_coeff ); + if( !pv_coeff.isNull() ){ + d_has_coeff.push_back( pv ); + } + } + void pop_back( Node pv, Node n, Node pv_coeff ){ + d_subs.pop_back(); + d_coeff.pop_back(); + if( !pv_coeff.isNull() ){ + d_has_coeff.pop_back(); + } + } + }; + // effort=0 : do not use model value, 1: use model value, 2: one must use model value + bool addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, + std::map< Node, Node >& cons, std::vector< Node >& curr_var ); + bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, + std::map< Node, Node >& cons, std::vector< Node >& curr_var ); + bool addInstantiationCoeff( SolvedForm& sf, + std::vector< Node >& vars, std::vector< int >& btyp, + unsigned j, std::map< Node, Node >& cons ); + bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ); + Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ); + Node applySubstitution( Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) { + return applySubstitution( n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff ); + } + Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, + std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ); + Node getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, + Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ); + void processAssertions(); + void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); + //get model value + Node getModelValue( Node n ); +public: + CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); + //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 ); +}; + +} +} +} + +#endif |