Enable counterexample-guided quantifier instantiation by default for quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.

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