From: Andrew Reynolds Date: Fri, 10 May 2013 02:39:03 +0000 (-0500) Subject: Add simplification option --fo-prop-quant. Add model support for new model-checking... X-Git-Tag: cvc5-1.0.0~7287^2~129 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=20cde072ebef5eddfc1562bebdd9438c77a22c8e;p=cvc5.git Add simplification option --fo-prop-quant. Add model support for new model-checking procedure. Add run script for casc24-fnt. --- 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& 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 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 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 + +#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 & lits ){ + if( n.getKind()==FORALL ){ + collectLits( n[1], lits ); + }else if( n.getKind()==OR ){ + for(unsigned j=0; j& assertions ){ + for( unsigned i=0; i 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; jmkConst(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 & lits) { + int index = -1; + for( unsigned i=0; imkConst( 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; imkNode( 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 +#include +#include +#include +#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 & 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; imkBoundVar( 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; jgetRepresentative( 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 ); };