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.

3 files changed, 18 insertions, 8 deletions

diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp
index 0d7f5005a..265026b39 100644
--- a/src/theory/rewriterules/theory_rewriterules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules.cpp
@@ -317,13 +317,14 @@ Answer TheoryRewriteRules::addWatchIfDontKnow(Node g0, const RuleInst* ri,
                                               const size_t gid){
   /** TODO: Should use the representative of g, but should I keep the
       mapping for myself? */
-  /* If it false in one model (current valuation) it's false for all */
-  if (useCurrentModel){
-    Node val = getValuation().getValue(g0);
-    Debug("rewriterules") << "getValue:" << g0 << " = "
-                          << val << " is " << (val == d_false) << std::endl;
-    if (val == d_false) return AFALSE;
-  };
+  //AJR: removed this code after talking with Francois
+  ///* If it false in one model (current valuation) it's false for all */
+  //if (useCurrentModel){
+  //  Node val = getValuation().getValue(g0);
+  //  Debug("rewriterules") << "getValue:" << g0 << " = "
+  //                        << val << " is " << (val == d_false) << std::endl;
+  //  if (val == d_false) return AFALSE;
+  //};
   /** Currently create a node with a literal */
   Node g = getValuation().ensureLiteral(g0);
   GuardedMap::iterator l_i = d_guardeds.find(g);
@@ -508,6 +509,10 @@ Node TheoryRewriteRules::explain(TNode n){
   return substGuards(&i, TCache ());
 }
 
+void TheoryRewriteRules::collectModelInfo( TheoryModel* m ){
+
+}
+
 Theory::PPAssertStatus TheoryRewriteRules::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   addRewriteRule(in);
   return PP_ASSERT_STATUS_UNSOLVED;
diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h
index e47fd2fd4..d1c3eecf3 100644
--- a/src/theory/rewriterules/theory_rewriterules.h
+++ b/src/theory/rewriterules/theory_rewriterules.h
@@ -30,6 +30,7 @@
 #include "theory/inst_match_impl.h"
 #include "util/stats.h"
 #include "theory/rewriterules/theory_rewriterules_preprocess.h"
+#include "theory/model.h"
 
 namespace CVC4 {
 namespace theory {
@@ -182,6 +183,7 @@ private:
       inside check */
   typedef std::vector< RuleInst* > QRuleInsts;
   QRuleInsts d_ruleinsts_to_add;
+
  public:
   /** true and false for predicate */
   Node d_true;
@@ -199,6 +201,7 @@ private:
   /** Usual function for theories */
   void check(Theory::Effort e);
   Node explain(TNode n);
+  void collectModelInfo( TheoryModel* m );
   void notifyEq(TNode lhs, TNode rhs);
   std::string identify() const {
     return "THEORY_REWRITERULES";
diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp
index d66fc78cb..c3116aba0 100644
--- a/src/theory/rewriterules/theory_rewriterules_rules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp
@@ -22,6 +22,8 @@
 #include "theory/rewriterules/theory_rewriterules_preprocess.h"
 #include "theory/rewriterules/theory_rewriterules.h"
 
+#include "theory/quantifiers/term_database.h"
+
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -72,7 +74,7 @@ inline void addPattern(TheoryRewriteRules & re,
                        TNode r){
   if (tri.getKind() == kind::NOT && tri[0].getKind() == kind::APPLY_UF)
     tri = tri[0];
-  pattern.push_back(re.getQuantifiersEngine()->
+  pattern.push_back(re.getQuantifiersEngine()->getTermDatabase()->
                     convertNodeToPattern(tri,r,vars,inst_constants));
 }