merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.

6 files changed, 201 insertions, 18 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index cded1e5a3..43cc15ec9 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -73,7 +73,9 @@ libutil_la_SOURCES = \
 	ite_removal.h \
 	ite_removal.cpp \
 	node_visitor.h \
-	index.h
+	index.h \
+	model.h \
+	model.cpp
 
 libutil_la_LIBADD = \
 	@builddir@/libutilcudd.la
diff --git a/src/util/dump.h b/src/util/dump.h
index 7318af1a5..382092474 100644
--- a/src/util/dump.h
+++ b/src/util/dump.h
@@ -103,7 +103,7 @@ public:
       std::string s = ss.str();
       CVC4dumpstream(getStream(), d_commands)
         << CommentCommand(s + " is " + comment)
-        << DeclareFunctionCommand(s, e.getType());
+        << DeclareFunctionCommand(s, e, e.getType());
     }
   }
 
diff --git a/src/util/model.cpp b/src/util/model.cpp
new file mode 100644
index 000000000..081624c5d
--- /dev/null
+++ b/src/util/model.cpp
@@ -0,0 +1,15 @@
+/*********************                                                        */

+/*! \file model.cpp

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)

+ ** Courant Institute of Mathematical Sciences

+ ** New York University

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief implementation of Model class

+ **/
\ No newline at end of file
diff --git a/src/util/model.h b/src/util/model.h
new file mode 100644
index 000000000..7e0f5a723
--- /dev/null
+++ b/src/util/model.h
@@ -0,0 +1,42 @@
+/*********************                                                        */

+/*! \file model.h

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)

+ ** Courant Institute of Mathematical Sciences

+ ** New York University

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Model class

+ **/

+

+#include "cvc4_public.h"

+

+#ifndef __CVC4__MODEL_H

+#define __CVC4__MODEL_H

+

+#include <iostream>

+

+namespace CVC4 {

+

+class Model

+{

+public:

+  virtual void toStream(std::ostream& out) = 0;

+};/* class Model */

+

+class ModelBuilder

+{

+public:

+  ModelBuilder(){}

+  virtual ~ModelBuilder(){}

+  virtual void buildModel( Model* m ) = 0;

+};/* class ModelBuilder */

+

+}/* CVC4 namespace */

+

+#endif  /* __CVC4__MODEL_H */

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 2352ae503..e9efab5dd 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -149,14 +149,22 @@ Options::Options() :
   instWhenMode(INST_WHEN_FULL_LAST_CALL),
   eagerInstQuant(false),
   finiteModelFind(false),
-  fmfRegionSat(false),
+  ufssEagerSplits(false),
+  ufssRegions(true),
+  ufssColoringSat(false),
   fmfModelBasedInst(true),
+  fmfInstGen(true),
+  fmfOneInstPerRound(false),
+  fmfInstEngine(false),
+  fmfRelevantDomain(false),
   efficientEMatching(false),
   literalMatchMode(LITERAL_MATCH_NONE),
   cbqi(false),
   cbqiSetByUser(false),
   userPatternsQuant(true),
   flipDecision(false),
+  printInstEngine(false),
+  printModelEngine(false),
   lemmaOutputChannel(NULL),
   lemmaInputChannel(NULL),
   threads(2),// default should be 1 probably, but say 2 for now
@@ -275,6 +283,7 @@ Additional CVC4 options:\n\
    --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al.,\n\
                           CADE 2011) [on by default only for QF_UF]\n\
    --disable-symmetry-breaker turns off UF symmetry breaker\n\
+ QUANTIFIERS:\n\
    --disable-miniscope-quant     disable miniscope quantifiers\n\
    --disable-miniscope-quant-fv  disable miniscope quantifiers for ground subformulas\n\
    --disable-prenex-quant disable prenexing of quantified formulas\n\
@@ -282,18 +291,26 @@ Additional CVC4 options:\n\
    --cnf-quant            apply CNF conversion to quantified formulas\n\
    --pre-skolem-quant     apply skolemization eagerly to bodies of quantified formulas\n\
    --disable-smart-triggers   disable smart triggers\n\
-   --register-quant-body-terms  consider terms within bodies of quantified formulas for matching\n\
+   --register-quant-body-terms  consider ground terms within bodies of quantified formulas for matching\n\
    --inst-when=MODE       when to apply instantiation\n\
    --eager-inst-quant     apply quantifier instantiation eagerly\n\
-   --finite-model-find    use finite model finding heuristic for quantifier instantiation\n\
-   --use-fmf-region-sat   use region-based SAT heuristic for finite model finding\n\
-   --disable-fmf-model-inst  disable model-based instantiation for finite model finding\n\
    --efficient-e-matching use efficient E-matching\n\
    --literal-matching=MODE  choose literal matching mode\n\
    --enable-cbqi          turns on counterexample-based quantifier instantiation [off by default]\n\
    --disable-cbqi         turns off counterexample-based quantifier instantiation\n\
    --ignore-user-patterns ignore user-provided patterns for quantifier instantiation\n\
    --enable-flip-decision turns on flip decision heuristic\n\
+ FINITE_MODEL_FINDING:\n\
+   --finite-model-find      use finite model finding heuristic for quantifier instantiation\n\
+   --disable-uf-ss-regions  disable region-based method for discovering cliques and splits in uf strong solver\n\
+   --uf-ss-eager-split      add splits eagerly for uf strong solver\n\
+   --uf-ss-coloring-sat     use coloring-based SAT heuristic for uf strong solver\n\
+   --disable-fmf-mbqi       disable model-based quantifier instantiation for finite model finding\n\
+   --disable-fmf-inst-gen   disable Inst-Gen instantiation techniques for finite model finding\n\
+   --fmf-one-inst-per-round  only add one instantiation per quantifier per round for fmf\n\
+   --fmf-inst-engine        use instantiation engine in conjunction with finite model finding\n\
+   --fmf-relevant-domain    use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)\n\
+ OTHER:\n\
    --disable-dio-solver   turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\
    --disable-arith-rewrite-equalities   turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n\
    --threads=N            sets the number of solver threads\n\
@@ -379,6 +396,36 @@ justification-must\n\
 + near leaves (don't expect it to work well) [Unimplemented]\n\
 ";
 
+static const string instWhenHelp = "\
+Modes currently supported by the --inst-when option:\n\
+\n\
+full\n\
++ Run instantiation round at full effort, before theory combination.\n\
+\n\
+full-last-call (default)\n\
++ Alternate running instantiation rounds at full effort and last\n\
+  call.  In other words, interleave instantiation and theory combination.\n\
+\n\
+last-call\n\
++ Run instantiation at last call effort, after theory combination.\n\
+\n\
+";
+
+static const string literalMatchHelp = "\
+Literal match modes currently supported by the --literal-match option:\n\
+\n\
+none (default)\n\
++ Do not use literal matching.\n\
+\n\
+predicate\n\
++ Consider the phase requirements of predicate literals when applying heuristic\n\
+  quantifier instantiation.  For example, the trigger P( x ) in the quantified \n\
+  formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\
+  terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\
+  Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\
+\n\
+";
+
 static const string dumpHelp = "\
 Dump modes currently supported by the --dump option:\n\
 \n\
@@ -581,14 +628,22 @@ enum OptionValue {
   INST_WHEN,
   EAGER_INST_QUANT,
   FINITE_MODEL_FIND,
-  FMF_REGION_SAT,
+  DISABLE_UF_SS_REGIONS,
+  UF_SS_EAGER_SPLIT,
+  UF_SS_COLORING_SAT,
   DISABLE_FMF_MODEL_BASED_INST,
+  DISABLE_FMF_INST_GEN,
+  FMF_ONE_INST_PER_ROUND,
+  FMF_INST_ENGINE,
+  FMF_RELEVANT_DOMAIN,
   EFFICIENT_E_MATCHING,
   LITERAL_MATCHING,
   ENABLE_CBQI,
   DISABLE_CBQI,
   IGNORE_USER_PATTERNS,
   ENABLE_FLIP_DECISION,
+  PRINT_MODEL_ENGINE,
+  PRINT_INST_ENGINE,
   PARALLEL_THREADS,
   PARALLEL_SEPARATE_OUTPUT,
   PORTFOLIO_FILTER_LENGTH,
@@ -710,14 +765,22 @@ static struct option cmdlineOptions[] = {
   { "inst-when", required_argument, NULL, INST_WHEN },
   { "eager-inst-quant", no_argument, NULL, EAGER_INST_QUANT },
   { "finite-model-find", no_argument, NULL, FINITE_MODEL_FIND },
-  { "use-fmf-region-sat", no_argument, NULL, FMF_REGION_SAT },
-  { "disable-fmf-model-inst", no_argument, NULL, DISABLE_FMF_MODEL_BASED_INST },
+  { "disable-uf-ss-regions", no_argument, NULL, DISABLE_UF_SS_REGIONS },
+  { "uf-ss-eager-split", no_argument, NULL, UF_SS_EAGER_SPLIT },
+  { "uf-ss-coloring-sat", no_argument, NULL, UF_SS_COLORING_SAT },
+  { "disable-fmf-mbqi", no_argument, NULL, DISABLE_FMF_MODEL_BASED_INST },
+  { "disable-fmf-inst-gen", no_argument, NULL, DISABLE_FMF_INST_GEN },
+  { "fmf-one-inst-per-round", no_argument, NULL, FMF_ONE_INST_PER_ROUND },
+  { "fmf-inst-engine", no_argument, NULL, FMF_INST_ENGINE },
+  { "fmf-relevant-domain", no_argument, NULL, FMF_RELEVANT_DOMAIN },
   { "efficient-e-matching", no_argument, NULL, EFFICIENT_E_MATCHING },
   { "literal-matching", required_argument, NULL, LITERAL_MATCHING },
   { "enable-cbqi", no_argument, NULL, ENABLE_CBQI },
   { "disable-cbqi", no_argument, NULL, DISABLE_CBQI },
   { "ignore-user-patterns", no_argument, NULL, IGNORE_USER_PATTERNS },
   { "enable-flip-decision", no_argument, NULL, ENABLE_FLIP_DECISION },
+  { "print-m-e", no_argument, NULL, PRINT_MODEL_ENGINE },
+  { "print-i-e", no_argument, NULL, PRINT_INST_ENGINE },
   { "threads", required_argument, NULL, PARALLEL_THREADS },
   { "separate-output", no_argument, NULL, PARALLEL_SEPARATE_OUTPUT },
   { "filter-lemma-length", required_argument, NULL, PORTFOLIO_FILTER_LENGTH },
@@ -1071,7 +1134,7 @@ throw(OptionException) {
       if(i == 0) {
         Warning() << "Decision budget is 0. Consider using internal decision heuristic and "
                   << std::endl << " removing this option." << std::endl;
-                  
+
       }
       decisionOptions.maxRelTimeAsPermille = (unsigned short)i;
     }
@@ -1247,7 +1310,7 @@ throw(OptionException) {
       } else if(!strcmp(optarg, "last-call")) {
         instWhenMode = INST_WHEN_LAST_CALL;
       } else if(!strcmp(optarg, "help")) {
-        //puts(instWhenHelp.c_str());
+        puts(instWhenHelp.c_str());
         exit(1);
       } else {
         throw OptionException(string("unknown option for --inst-when: `") +
@@ -1260,12 +1323,30 @@ throw(OptionException) {
     case FINITE_MODEL_FIND:
       finiteModelFind = true;
       break;
-    case FMF_REGION_SAT:
-      fmfRegionSat = true;
+    case DISABLE_UF_SS_REGIONS:
+      ufssRegions = false;
+      break;
+    case UF_SS_EAGER_SPLIT:
+      ufssEagerSplits = true;
+      break;
+    case UF_SS_COLORING_SAT:
+      ufssColoringSat = true;
       break;
     case DISABLE_FMF_MODEL_BASED_INST:
       fmfModelBasedInst = false;
       break;
+    case DISABLE_FMF_INST_GEN:
+      fmfInstGen = false;
+      break;
+    case FMF_ONE_INST_PER_ROUND:
+      fmfOneInstPerRound = true;
+      break;
+    case FMF_INST_ENGINE:
+      fmfInstEngine = true;
+      break;
+    case FMF_RELEVANT_DOMAIN:
+      fmfRelevantDomain = true;
+      break;
     case EFFICIENT_E_MATCHING:
       efficientEMatching = true;
       break;
@@ -1277,7 +1358,7 @@ throw(OptionException) {
       } else if(!strcmp(optarg, "equality")) {
         literalMatchMode = LITERAL_MATCH_EQUALITY;
       } else if(!strcmp(optarg, "help")) {
-        //puts(literalMatchHelp.c_str());
+        puts(literalMatchHelp.c_str());
         exit(1);
       } else {
         throw OptionException(string("unknown option for --literal-matching: `") +
@@ -1298,6 +1379,12 @@ throw(OptionException) {
     case ENABLE_FLIP_DECISION:
       flipDecision = true;
       break;
+    case PRINT_MODEL_ENGINE:
+      printModelEngine = true;
+      break;
+    case PRINT_INST_ENGINE:
+      printInstEngine = true;
+      break;
     case TIME_LIMIT:
       {
         int i = atoi(optarg);
diff --git a/src/util/options.h b/src/util/options.h
index f423260b0..d89265b55 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -147,7 +147,7 @@ struct CVC4_PUBLIC Options {
   DecisionMode decisionMode;
   /** Whether the user set the decision strategy */
   bool decisionModeSetByUser;
-  /** 
+  /**
    * Extra settings for decision stuff, varies by strategy enabled
    * - With DECISION_STRATEGY_RELEVANCY
    *   > Least significant bit: true if one should only decide on leaves
@@ -414,9 +414,20 @@ struct CVC4_PUBLIC Options {
   bool finiteModelFind;
 
   /**
-   * Whether to use region-based SAT for finite model finding
+   * Whether to use eager splitting on demand for finite model finding
+   */
+  bool ufssEagerSplits;
+
+  /**
+   * Whether to use region-based approach for finite model finding
+   */
+  bool ufssRegions;
+
+  /**
+   * Whether to use coloring-based methods for determining whether a model of
+   * currently cardinality exists.
    */
-  bool fmfRegionSat;
+  bool ufssColoringSat;
 
   /**
    * Whether to use model-based exhaustive instantiation for finite model finding
@@ -424,6 +435,26 @@ struct CVC4_PUBLIC Options {
   bool fmfModelBasedInst;
 
   /**
+   * Whether to use Inst-Gen techniques for finite model finding
+   */
+  bool fmfInstGen;
+
+  /*
+   * Whether to only add only instantiation per quantifier per round for finite model finding
+   */
+  bool fmfOneInstPerRound;
+
+  /*
+   * Whether to use instantiation engine in conjunction with finite model finding
+   */
+  bool fmfInstEngine;
+
+  /*
+   * Whether to compute relevant domains, in the manner of Complete Instantiation for Quantified Formulas [Ge, deMoura 09]
+   */
+  bool fmfRelevantDomain;
+
+  /**
    * Whether to use efficient E-matching
    */
   bool efficientEMatching;
@@ -462,6 +493,12 @@ struct CVC4_PUBLIC Options {
    */
   bool flipDecision;
 
+  /**
+   * print details for instantiation/model engine
+   */
+  bool printInstEngine;
+  bool printModelEngine;
+
   /** The output channel to receive notfication events for new lemmas */
   LemmaOutputChannel* lemmaOutputChannel;
   LemmaInputChannel* lemmaInputChannel;