--- /dev/null
+#!/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
+;;
+
+
#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;
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();
}
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 (;;) {
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(): "
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]);
}
}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 );
}
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();
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;
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 \
}\r
\r
void BoundedIntegers::registerQuantifier( Node f ) {\r
+ Trace("bound-integers") << "Register quantifier " << f << std::endl;\r
bool hasIntType = false;\r
for( unsigned i=0; i<f[0].getNumChildren(); i++) {\r
if( f[0][i].getType().isInteger() ){\r
--- /dev/null
+/********************* */\r
+/*! \file first_order_reasoning.cpp\r
+ ** \verbatim\r
+ ** Original author: ajreynol\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief first order reasoning module\r
+ **\r
+ **/\r
+\r
+#include <vector>\r
+\r
+#include "theory/quantifiers/first_order_reasoning.h"\r
+#include "theory/rewriter.h"\r
+\r
+using namespace CVC4;\r
+using namespace CVC4::kind;\r
+using namespace std;\r
+\r
+namespace CVC4 {\r
+\r
+\r
+void FirstOrderPropagation::collectLits( Node n, std::vector<Node> & lits ){\r
+ if( n.getKind()==FORALL ){\r
+ collectLits( n[1], lits );\r
+ }else if( n.getKind()==OR ){\r
+ for(unsigned j=0; j<n.getNumChildren(); j++) {\r
+ collectLits(n[j], lits );\r
+ }\r
+ }else{\r
+ lits.push_back( n );\r
+ }\r
+}\r
+\r
+void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){\r
+ for( unsigned i=0; i<assertions.size(); i++) {\r
+ Trace("fo-rsn") << "Assert : " << assertions[i] << std::endl;\r
+ }\r
+\r
+ //process all assertions\r
+ int num_processed;\r
+ int num_true = 0;\r
+ int num_rounds = 0;\r
+ do {\r
+ num_processed = 0;\r
+ for( unsigned i=0; i<assertions.size(); i++ ){\r
+ if( d_assertion_true.find(assertions[i])==d_assertion_true.end() ){\r
+ std::vector< Node > fo_lits;\r
+ collectLits( assertions[i], fo_lits );\r
+ Node unitLit = process( assertions[i], fo_lits );\r
+ if( !unitLit.isNull() ){\r
+ Trace("fo-rsn-debug") << "...possible unit literal : " << unitLit << " from " << assertions[i] << std::endl;\r
+ bool pol = unitLit.getKind()!=NOT;\r
+ unitLit = unitLit.getKind()==NOT ? unitLit[0] : unitLit;\r
+ if( unitLit.getKind()==EQUAL ){\r
+\r
+ }else if( unitLit.getKind()==APPLY_UF ){\r
+ //make sure all are unique vars;\r
+ bool success = true;\r
+ std::vector< Node > unique_vars;\r
+ for( unsigned j=0; j<unitLit.getNumChildren(); j++) {\r
+ if( unitLit[j].getKind()==BOUND_VARIABLE ){\r
+ if( std::find(unique_vars.begin(), unique_vars.end(), unitLit[j])==unique_vars.end() ){\r
+ unique_vars.push_back( unitLit[j] );\r
+ }else{\r
+ success = false;\r
+ break;\r
+ }\r
+ }else{\r
+ success = false;\r
+ break;\r
+ }\r
+ }\r
+ if( success ){\r
+ d_const_def[unitLit.getOperator()] = NodeManager::currentNM()->mkConst(pol);\r
+ Trace("fo-rsn") << "Propagate : " << unitLit.getOperator() << " == " << pol << std::endl;\r
+ Trace("fo-rsn") << " from : " << assertions[i] << std::endl;\r
+ d_assertion_true[assertions[i]] = true;\r
+ num_processed++;\r
+ }\r
+ }else if( unitLit.getKind()==VARIABLE ){\r
+ d_const_def[unitLit] = NodeManager::currentNM()->mkConst(pol);\r
+ Trace("fo-rsn") << "Propagate variable : " << unitLit << " == " << pol << std::endl;\r
+ Trace("fo-rsn") << " from : " << assertions[i] << std::endl;\r
+ d_assertion_true[assertions[i]] = true;\r
+ num_processed++;\r
+ }\r
+ }\r
+ if( d_assertion_true.find(assertions[i])!=d_assertion_true.end() ){\r
+ num_true++;\r
+ }\r
+ }\r
+ }\r
+ num_rounds++;\r
+ }while( num_processed>0 );\r
+ Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl;\r
+ for( unsigned i=0; i<assertions.size(); i++ ){\r
+ assertions[i] = theory::Rewriter::rewrite( simplify( assertions[i] ) );\r
+ }\r
+}\r
+\r
+Node FirstOrderPropagation::process(Node a, std::vector< Node > & lits) {\r
+ int index = -1;\r
+ for( unsigned i=0; i<lits.size(); i++) {\r
+ bool pol = lits[i].getKind()!=NOT;\r
+ Node n = lits[i].getKind()==NOT ? lits[i][0] : lits[i];\r
+ Node litDef;\r
+ if( n.getKind()==APPLY_UF ){\r
+ if( d_const_def.find(n.getOperator())!=d_const_def.end() ){\r
+ litDef = d_const_def[n.getOperator()];\r
+ }\r
+ }else if( n.getKind()==VARIABLE ){\r
+ if( d_const_def.find(n)!=d_const_def.end() ){\r
+ litDef = d_const_def[n];\r
+ }\r
+ }\r
+ if( !litDef.isNull() ){\r
+ Node poln = NodeManager::currentNM()->mkConst( pol );\r
+ if( litDef==poln ){\r
+ Trace("fo-rsn-debug") << "Assertion " << a << " is true because of " << lits[i] << std::endl;\r
+ d_assertion_true[a] = true;\r
+ return Node::null();\r
+ }\r
+ }\r
+ if( litDef.isNull() ){\r
+ if( index==-1 ){\r
+ //store undefined index\r
+ index = i;\r
+ }else{\r
+ //two undefined, return null\r
+ return Node::null();\r
+ }\r
+ }\r
+ }\r
+ if( index!=-1 ){\r
+ return lits[index];\r
+ }else{\r
+ return Node::null();\r
+ }\r
+}\r
+\r
+Node FirstOrderPropagation::simplify( Node n ) {\r
+ if( n.getKind()==VARIABLE ){\r
+ if( d_const_def.find(n)!=d_const_def.end() ){\r
+ return d_const_def[n];\r
+ }\r
+ }else if( n.getKind()==APPLY_UF ){\r
+ if( d_const_def.find(n.getOperator())!=d_const_def.end() ){\r
+ return d_const_def[n.getOperator()];\r
+ }\r
+ }\r
+ if( n.getNumChildren()==0 ){\r
+ return n;\r
+ }else{\r
+ std::vector< Node > children;\r
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){\r
+ children.push_back( n.getOperator() );\r
+ }\r
+ for(unsigned i=0; i<n.getNumChildren(); i++) {\r
+ children.push_back( simplify(n[i]) );\r
+ }\r
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );\r
+ }\r
+}\r
+\r
+}\r
--- /dev/null
+/********************* */\r
+/*! \file first_order_reasoning.h\r
+ ** \verbatim\r
+ ** Original author: ajreynol\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Pre-process step for first-order reasoning\r
+ **/\r
+\r
+#include "cvc4_private.h"\r
+\r
+#ifndef __CVC4__FIRST_ORDER_REASONING_H\r
+#define __CVC4__FIRST_ORDER_REASONING_H\r
+\r
+#include <iostream>\r
+#include <string>\r
+#include <vector>\r
+#include <map>\r
+#include "expr/node.h"\r
+#include "expr/type_node.h"\r
+\r
+namespace CVC4 {\r
+\r
+class FirstOrderPropagation {\r
+private:\r
+ std::map< Node, Node > d_const_def;\r
+ std::map< Node, bool > d_assertion_true;\r
+ Node process(Node a, std::vector< Node > & lits);\r
+ void collectLits( Node n, std::vector<Node> & lits );\r
+ Node simplify( Node n );\r
+public:\r
+ FirstOrderPropagation(){}\r
+ ~FirstOrderPropagation(){}\r
+\r
+ void simplify( std::vector< Node >& assertions );\r
+};\r
+\r
+}\r
+\r
+#endif\r
}\r
}\r
}else{\r
- //TODO\r
+ Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;\r
Trace("fmc-exh") << "Definition was : " << std::endl;\r
d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);\r
Trace("fmc-exh") << std::endl;\r
bool FullModelChecker::useSimpleModels() {\r
return options::fmfFullModelCheckSimple();\r
}\r
+\r
+Node FullModelChecker::getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix ) {\r
+ TypeNode type = op.getType();\r
+ std::vector< Node > vars;\r
+ for( size_t i=0; i<type.getNumChildren()-1; i++ ){\r
+ std::stringstream ss;\r
+ ss << argPrefix << (i+1);\r
+ vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );\r
+ }\r
+ Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);\r
+ Node curr;\r
+ for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {\r
+ Node v = fm->getRepresentative( d_models[op]->d_value[i] );\r
+ if( curr.isNull() ){\r
+ curr = v;\r
+ }else{\r
+ //make the condition\r
+ Node cond = d_models[op]->d_cond[i];\r
+ std::vector< Node > children;\r
+ for( unsigned j=0; j<cond.getNumChildren(); j++) {\r
+ if (!isStar(cond[j])){\r
+ Node c = fm->getRepresentative( cond[j] );\r
+ children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );\r
+ }\r
+ }\r
+ Assert( !children.empty() );\r
+ Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );\r
+ curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );\r
+ }\r
+ }\r
+ curr = Rewriter::rewrite( curr );\r
+ return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);\r
+}
\ No newline at end of file
\r
bool isActive();\r
bool useSimpleModels();\r
+ Node getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix );\r
};\r
\r
}\r
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
# 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
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 );
};
projects / cvc5.git / commitdiff