11 files changed, 315 insertions, 26 deletions
diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt
new file mode 100755
index 000000000..0230b8e13
--- /dev/null
+++ b/contrib/run-script-casc24-fnt
@@ -0,0 +1,27 @@
+#!/bin/bash
+
+cvc4=cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+# use: trywith [params..]
+# to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
+# which case this run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  result="$($cvc4 -L tptp --no-checking --no-interactive "$@" $bench)"
+  case "$result" in
+    sat) echo "SZS Satisfiable for $filename"; exit 0;;
+    unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
+  esac
+}
+
+
+trywith --finite-model-find --uf-ss-totality --tlimit-per=10000
+trywith --finite-model-find --decision=justification --tlimit-per=10000
+trywith --finite-model-find --decision=justification --fmf-fmc
+;;
+
+
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 37ab9cd48..e49e6fb54 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -74,6 +74,7 @@
 #include "util/sort_inference.h"
 #include "theory/quantifiers/macros.h"
 #include "theory/datatypes/options.h"
+#include "theory/quantifiers/first_order_reasoning.h"
 
 using namespace std;
 using namespace CVC4;
@@ -349,8 +350,8 @@ private:
   bool checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache);
 
   // Lift bit-vectors of size 1 to booleans
-  void bvToBool(); 
-  
+  void bvToBool();
+
   // Simplify ITE structure
   void simpITE();
 
@@ -1832,15 +1833,15 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   }
 
   hash_set<TNode, TNodeHashFunction> s;
-  Trace("debugging") << "NonClausal simplify pre-preprocess\n"; 
+  Trace("debugging") << "NonClausal simplify pre-preprocess\n";
   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
     Node assertion = d_assertionsToPreprocess[i];
     Node assertionNew = d_topLevelSubstitutions.apply(assertion);
     Trace("debugging") << "assertion = " << assertion << endl;
-    Trace("debugging") << "assertionNew = " << assertionNew << endl; 
+    Trace("debugging") << "assertionNew = " << assertionNew << endl;
     if (assertion != assertionNew) {
       assertion = Rewriter::rewrite(assertionNew);
-      Trace("debugging") << "rewrite(assertion) = " << assertion << endl; 
+      Trace("debugging") << "rewrite(assertion) = " << assertion << endl;
     }
     Assert(Rewriter::rewrite(assertion) == assertion);
     for (;;) {
@@ -1849,11 +1850,11 @@ bool SmtEnginePrivate::nonClausalSimplify() {
         break;
       }
       ++d_smt.d_stats->d_numConstantProps;
-      Trace("debugging") << "assertionNew = " << assertionNew << endl; 
+      Trace("debugging") << "assertionNew = " << assertionNew << endl;
       assertion = Rewriter::rewrite(assertionNew);
-      Trace("debugging") << "assertionNew = " << assertionNew << endl; 
+      Trace("debugging") << "assertionNew = " << assertionNew << endl;
     }
-    Trace("debugging") << "\n"; 
+    Trace("debugging") << "\n";
     s.insert(assertion);
     d_assertionsToCheck.push_back(assertion);
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
@@ -1944,7 +1945,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
 void SmtEnginePrivate::bvToBool() {
   Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl;
   std::vector<Node> new_assertions;
-  d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions); 
+  d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions);
   for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
     d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]);
   }
@@ -2798,6 +2799,12 @@ void SmtEnginePrivate::processAssertions() {
     }while( success );
   }
 
+  Trace("fo-rsn-enable") << std::endl;
+  if( options::foPropQuant() ){
+    FirstOrderPropagation fop;
+    fop.simplify( d_assertionsToPreprocess );
+  }
+
   if( options::sortInference() ){
     //sort inference technique
     d_smt.d_theoryEngine->getSortInference()->simplify( d_assertionsToPreprocess );
@@ -2818,7 +2825,7 @@ void SmtEnginePrivate::processAssertions() {
   }
   dumpAssertions("post-static-learning", d_assertionsToCheck);
 
-  // Lift bit-vectors of size 1 to bool 
+  // Lift bit-vectors of size 1 to bool
   if(options::bvToBool()) {
     Chat() << "...doing bvToBool..." << endl;
     bvToBool();
@@ -2828,7 +2835,7 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
-  
+
   dumpAssertions("pre-ite-removal", d_assertionsToCheck);
   {
     Chat() << "removing term ITEs..." << endl;
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index 1a1413ad6..92d780be4 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -48,7 +48,9 @@ libquantifiers_la_SOURCES = \
 	full_model_check.h \
 	full_model_check.cpp \
 	bounded_integers.h \
-	bounded_integers.cpp
+	bounded_integers.cpp \
+	first_order_reasoning.h \
+	first_order_reasoning.cpp
 
 EXTRA_DIST = \
 	kinds \
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 7af6456b6..03a52539e 100755
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -77,6 +77,7 @@ void BoundedIntegers::check( Theory::Effort e ) {
 }
 
 void BoundedIntegers::registerQuantifier( Node f ) {
+  Trace("bound-integers") << "Register quantifier " << f << std::endl;
   bool hasIntType = false;
   for( unsigned i=0; i<f[0].getNumChildren(); i++) {
     if( f[0][i].getType().isInteger() ){
diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp
new file mode 100755
index 000000000..27fcebccf
--- /dev/null
+++ b/src/theory/quantifiers/first_order_reasoning.cpp
@@ -0,0 +1,171 @@
+/*********************                                                        */
+/*! \file first_order_reasoning.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-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief first order reasoning module
+ **
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/first_order_reasoning.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace std;
+
+namespace CVC4 {
+
+
+void FirstOrderPropagation::collectLits( Node n, std::vector<Node> & lits ){
+  if( n.getKind()==FORALL ){
+    collectLits( n[1], lits );
+  }else if( n.getKind()==OR ){
+    for(unsigned j=0; j<n.getNumChildren(); j++) {
+      collectLits(n[j], lits );
+    }
+  }else{
+    lits.push_back( n );
+  }
+}
+
+void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){
+  for( unsigned i=0; i<assertions.size(); i++) {
+    Trace("fo-rsn") << "Assert : " << assertions[i] << std::endl;
+  }
+
+  //process all assertions
+  int num_processed;
+  int num_true = 0;
+  int num_rounds = 0;
+  do {
+    num_processed = 0;
+    for( unsigned i=0; i<assertions.size(); i++ ){
+      if( d_assertion_true.find(assertions[i])==d_assertion_true.end() ){
+        std::vector< Node > fo_lits;
+        collectLits( assertions[i], fo_lits );
+        Node unitLit = process( assertions[i], fo_lits );
+        if( !unitLit.isNull() ){
+          Trace("fo-rsn-debug") << "...possible unit literal : " << unitLit << " from " << assertions[i] << std::endl;
+          bool pol = unitLit.getKind()!=NOT;
+          unitLit = unitLit.getKind()==NOT ? unitLit[0] : unitLit;
+          if( unitLit.getKind()==EQUAL ){
+
+          }else if( unitLit.getKind()==APPLY_UF ){
+            //make sure all are unique vars;
+            bool success = true;
+            std::vector< Node > unique_vars;
+            for( unsigned j=0; j<unitLit.getNumChildren(); j++) {
+              if( unitLit[j].getKind()==BOUND_VARIABLE ){
+                if( std::find(unique_vars.begin(), unique_vars.end(), unitLit[j])==unique_vars.end() ){
+                  unique_vars.push_back( unitLit[j] );
+                }else{
+                  success = false;
+                  break;
+                }
+              }else{
+                success = false;
+                break;
+              }
+            }
+            if( success ){
+              d_const_def[unitLit.getOperator()] = NodeManager::currentNM()->mkConst(pol);
+              Trace("fo-rsn") << "Propagate : " << unitLit.getOperator() << " == " << pol << std::endl;
+              Trace("fo-rsn") << "    from : " << assertions[i] << std::endl;
+              d_assertion_true[assertions[i]] = true;
+              num_processed++;
+            }
+          }else if( unitLit.getKind()==VARIABLE ){
+            d_const_def[unitLit] = NodeManager::currentNM()->mkConst(pol);
+            Trace("fo-rsn") << "Propagate variable : " << unitLit << " == " << pol << std::endl;
+            Trace("fo-rsn") << "    from : " << assertions[i] << std::endl;
+            d_assertion_true[assertions[i]] = true;
+            num_processed++;
+          }
+        }
+        if( d_assertion_true.find(assertions[i])!=d_assertion_true.end() ){
+          num_true++;
+        }
+      }
+    }
+    num_rounds++;
+  }while( num_processed>0 );
+  Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl;
+  for( unsigned i=0; i<assertions.size(); i++ ){
+    assertions[i] = theory::Rewriter::rewrite( simplify( assertions[i] ) );
+  }
+}
+
+Node FirstOrderPropagation::process(Node a, std::vector< Node > & lits) {
+  int index = -1;
+  for( unsigned i=0; i<lits.size(); i++) {
+    bool pol = lits[i].getKind()!=NOT;
+    Node n = lits[i].getKind()==NOT ? lits[i][0] : lits[i];
+    Node litDef;
+    if( n.getKind()==APPLY_UF ){
+      if( d_const_def.find(n.getOperator())!=d_const_def.end() ){
+        litDef = d_const_def[n.getOperator()];
+      }
+    }else if( n.getKind()==VARIABLE ){
+      if( d_const_def.find(n)!=d_const_def.end() ){
+        litDef = d_const_def[n];
+      }
+    }
+    if( !litDef.isNull() ){
+      Node poln = NodeManager::currentNM()->mkConst( pol );
+      if( litDef==poln ){
+        Trace("fo-rsn-debug") << "Assertion " << a << " is true because of " << lits[i] << std::endl;
+        d_assertion_true[a] = true;
+        return Node::null();
+      }
+    }
+    if( litDef.isNull() ){
+      if( index==-1 ){
+        //store undefined index
+        index = i;
+      }else{
+        //two undefined, return null
+        return Node::null();
+      }
+    }
+  }
+  if( index!=-1 ){
+    return lits[index];
+  }else{
+    return Node::null();
+  }
+}
+
+Node FirstOrderPropagation::simplify( Node n ) {
+  if( n.getKind()==VARIABLE ){
+    if( d_const_def.find(n)!=d_const_def.end() ){
+      return d_const_def[n];
+    }
+  }else if( n.getKind()==APPLY_UF ){
+    if( d_const_def.find(n.getOperator())!=d_const_def.end() ){
+      return d_const_def[n.getOperator()];
+    }
+  }
+  if( n.getNumChildren()==0 ){
+    return n;
+  }else{
+    std::vector< Node > children;
+    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      children.push_back( n.getOperator() );
+    }
+    for(unsigned i=0; i<n.getNumChildren(); i++) {
+      children.push_back( simplify(n[i]) );
+    }
+    return NodeManager::currentNM()->mkNode( n.getKind(), children );
+  }
+}
+
+}
diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h
new file mode 100755
index 000000000..0dbf23a3b
--- /dev/null
+++ b/src/theory/quantifiers/first_order_reasoning.h
@@ -0,0 +1,45 @@
+/*********************                                                        */
+/*! \file first_order_reasoning.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-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Pre-process step for first-order reasoning
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__FIRST_ORDER_REASONING_H
+#define __CVC4__FIRST_ORDER_REASONING_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+class FirstOrderPropagation {
+private:
+  std::map< Node, Node > d_const_def;
+  std::map< Node, bool > d_assertion_true;
+  Node process(Node a, std::vector< Node > & lits);
+  void collectLits( Node n, std::vector<Node> & lits );
+  Node simplify( Node n );
+public:
+  FirstOrderPropagation(){}
+  ~FirstOrderPropagation(){}
+
+  void simplify( std::vector< Node >& assertions );
+};
+
+}
+
+#endif
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index efd193fc5..4ce9dba21 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -507,7 +507,7 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, int ef
       }
     }
   }else{
-    //TODO
+    Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;
     Trace("fmc-exh") << "Definition was : " << std::endl;
     d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);
     Trace("fmc-exh") << std::endl;
@@ -941,3 +941,36 @@ bool FullModelChecker::isActive() {
 bool FullModelChecker::useSimpleModels() {
   return options::fmfFullModelCheckSimple();
 }
+
+Node FullModelChecker::getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix ) {
+  TypeNode type = op.getType();
+  std::vector< Node > vars;
+  for( size_t i=0; i<type.getNumChildren()-1; i++ ){
+    std::stringstream ss;
+    ss << argPrefix << (i+1);
+    vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
+  }
+  Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
+  Node curr;
+  for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
+    Node v = fm->getRepresentative( d_models[op]->d_value[i] );
+    if( curr.isNull() ){
+      curr = v;
+    }else{
+      //make the condition
+      Node cond = d_models[op]->d_cond[i];
+      std::vector< Node > children;
+      for( unsigned j=0; j<cond.getNumChildren(); j++) {
+        if (!isStar(cond[j])){
+          Node c = fm->getRepresentative( cond[j] );
+          children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
+        }
+      }
+      Assert( !children.empty() );
+      Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );
+      curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );
+    }
+  }
+  curr = Rewriter::rewrite( curr );
+  return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
+}
+\ No newline at end of file
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 3f54b0574..bf9ed94e4 100755
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -140,6 +140,7 @@ public:
 
   bool isActive();
   bool useSimpleModels();
+  Node getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix );
 };
 
 }
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 059c76b21..25e07de5d 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -92,12 +92,18 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
   FirstOrderModel* fm = (FirstOrderModel*)m;
   if( fullModel ){
     Assert( d_curr_model==fm );
-    //update models
-    for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
-      it->second.update( fm );
-      Trace("model-func") << "ModelEngineBuilder: Make function value from tree " << it->first << std::endl;
-      //construct function values
-      fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
+    if( d_qe->getModelEngine()->getFullModelChecker()->isActive() ){
+      for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+        fm->d_uf_models[ it->first ] = d_qe->getModelEngine()->getFullModelChecker()->getFunctionValue( fm, it->first, "$x" );
+      }
+    }else{
+      //update models
+      for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+        it->second.update( fm );
+        Trace("model-func") << "ModelEngineBuilder: Make function value from tree " << it->first << std::endl;
+        //construct function values
+        fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
+      }
     }
     TheoryEngineModelBuilder::processBuildModel( m, fullModel );
     //mark that the model has been set
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index a9b7f269f..6bbcb2c3d 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -47,6 +47,9 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
 # Whether to perform quantifier macro expansion
 option macrosQuant --macros-quant bool :default false
  perform quantifiers macro expansions
+# Whether to perform first-order propagation
+option foPropQuant --fo-prop-quant bool :default false
+ perform first-order propagation on quantifiers
 
 # Whether to use smart triggers
 option smartTriggers /--disable-smart-triggers bool :default true
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 9140806ec..2149a6583 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -144,13 +144,6 @@ public:
   void debugPrint( std::ostream& out, TheoryModel* m, int ind = 0 ){
     d_tree.debugPrint( out, m, d_index_order, ind );
   }
-private:
-  //helper for to ITE function.
-  static Node toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode );
-public:
-  /** to ITE function for function model nodes */
-  static Node toIte( Node fm_node, std::vector< Node >& args ) { return toIte2( fm_node, args, 0, Node::null() ); }
-  static Node toIte( TypeNode type, Node fm_node, const char* argPrefix );
 };