Add simplification option --fo-prop-quant. Add model support for new model-checking procedure. Add run script for casc24-fnt.

8 files changed, 270 insertions, 8 deletions

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