summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Makefile.am4
-rw-r--r--src/util/dump.h2
-rw-r--r--src/util/model.cpp15
-rw-r--r--src/util/model.h42
-rw-r--r--src/util/options.cpp113
-rw-r--r--src/util/options.h43
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback