if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
}
-trywith 30 --finite-model-find
-trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality --decision=internal
-trywith 10 --finite-model-find --disable-uf-ss-min-model
-trywith $to --finite-model-find --mbqi=abs --pre-skolem-quant
+trywith 30 --finite-model-find --sort-inference --uf-ss-fair
+trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality --decision=internal --sort-inference --uf-ss-fair
+trywith 10 --finite-model-find --disable-uf-ss-min-model --sort-inference --uf-ss-fair
+trywith $to --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair
echo "% SZS status" "GaveUp for $filename"
file=${bench##*/}
filename=${file%.*}
-echo "Run $bench at $2"
-
# 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 trywith {
limit=$1; shift;
echo "--- Run $@ at $limit...";
- (ulimit -t "$limit";$cvc4 --no-checking --no-interactive "$@" $bench) 2>/dev/null |
+ (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench) 2>/dev/null |
(read w1 w2 w3 result w4 w5;
case "$result" in
Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
#!/bin/bash
-cvc4=./cvc4
+cvc4=cvc4
bench="$1"
-let "to = $2 - 150"
+let "to = $2 - 170"
file=${bench##*/}
filename=${file%.*}
function trywith {
limit=$1; shift;
echo "--- Run $@ at $limit...";
- (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-models --produce-models "$@" $bench) 2>/dev/null |
+ (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench) 2>/dev/null |
(read w1 w2 w3 result w4 w5;
case "$result" in
Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
}
-trywith 30 --full-saturate-quant
-trywith 120 --quant-cf --qcf-tconstraint --full-saturate-quant
-trywith $to --cbqi --cbqi-recurse --full-saturate-quant --flip-decision
+trywith 15 --cbqi-recurse --full-saturate-quant
+trywith 15 --decision=internal --full-saturate-quant
+trywith 30 --quant-cf --qcf-tconstraint --full-saturate-quant
+trywith 20 --finite-model-find
+trywith 90 --full-saturate-quant
+trywith $to --cbqi-recurse --full-saturate-quant --pre-skolem-quant
echo "% SZS status" "GaveUp for $filename"
printer/printer.cpp \
printer/dagification_visitor.h \
printer/dagification_visitor.cpp \
- printer/model_format_mode.h \
- printer/model_format_mode.cpp \
+ printer/modes.h \
+ printer/modes.cpp \
printer/ast/ast_printer.h \
printer/ast/ast_printer.cpp \
printer/smt1/smt1_printer.h \
void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() {
try {
- smtEngine->printInstantiations();
+ d_smtEngine = smtEngine;
d_commandStatus = CommandSuccess::instance();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
- //d_result->toStream(out);
+ d_smtEngine->printInstantiations(out);
}
}
Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
GetInstantiationsCommand* c = new GetInstantiationsCommand();
//c->d_result = d_result;
+ c->d_smtEngine = d_smtEngine;
return c;
}
Command* GetInstantiationsCommand::clone() const {
GetInstantiationsCommand* c = new GetInstantiationsCommand();
//c->d_result = d_result;
+ c->d_smtEngine = d_smtEngine;
return c;
}
class CVC4_PUBLIC GetInstantiationsCommand : public Command {
protected:
//Instantiations* d_result;
+ SmtEngine* d_smtEngine;
public:
GetInstantiationsCommand() throw();
~GetInstantiationsCommand() throw() {}
Command* gp = new GetProofCommand();
status = doCommandSingleton(gp);
} else if( d_options[options::dumpInstantiations] &&
- d_result.asSatisfiabilityResult() == Result::UNSAT ) {
+ res.asSatisfiabilityResult() == Result::UNSAT ) {
Command* gi = new GetInstantiationsCommand();
status = doCommandSingleton(gi);
}
+++ /dev/null
-/********************* */
-/*! \file model_format_mode.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "printer/model_format_mode.h"
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) {
- switch(mode) {
- case MODEL_FORMAT_MODE_DEFAULT:
- out << "MODEL_FORMAT_MODE_DEFAULT";
- break;
- case MODEL_FORMAT_MODE_TABLE:
- out << "MODEL_FORMAT_MODE_TABLE";
- break;
- default:
- out << "ModelFormatMode:UNKNOWN![" << unsigned(mode) << "]";
- }
-
- return out;
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file model_format_mode.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__PRINTER__MODEL_FORMAT_MODE_H
-#define __CVC4__PRINTER__MODEL_FORMAT_MODE_H
-
-#include <iostream>
-
-namespace CVC4 {
-
-/** Enumeration of model_format modes (how to print models from get-model command). */
-typedef enum {
- /** default mode (print expressions in the output language format) */
- MODEL_FORMAT_MODE_DEFAULT,
- /** print functional values in a table format */
- MODEL_FORMAT_MODE_TABLE,
-} ModelFormatMode;
-
-std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PRINTER__MODEL_FORMAT_H */
--- /dev/null
+/********************* */
+/*! \file modes.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "printer/modes.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) {
+ switch(mode) {
+ case MODEL_FORMAT_MODE_DEFAULT:
+ out << "MODEL_FORMAT_MODE_DEFAULT";
+ break;
+ case MODEL_FORMAT_MODE_TABLE:
+ out << "MODEL_FORMAT_MODE_TABLE";
+ break;
+ default:
+ out << "ModelFormatMode:UNKNOWN![" << unsigned(mode) << "]";
+ }
+
+ return out;
+}
+
+std::ostream& operator<<(std::ostream& out, InstFormatMode mode) {
+ switch(mode) {
+ case INST_FORMAT_MODE_DEFAULT:
+ out << "INST_FORMAT_MODE_DEFAULT";
+ break;
+ case INST_FORMAT_MODE_SZS:
+ out << "INST_FORMAT_MODE_SZS";
+ break;
+ default:
+ out << "InstFormatMode:UNKNOWN![" << unsigned(mode) << "]";
+ }
+ return out;
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file modes.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__PRINTER__MODES_H
+#define __CVC4__PRINTER__MODES_H
+
+#include <iostream>
+
+namespace CVC4 {
+
+/** Enumeration of model_format modes (how to print models from get-model command). */
+typedef enum {
+ /** default mode (print expressions in the output language format) */
+ MODEL_FORMAT_MODE_DEFAULT,
+ /** print functional values in a table format */
+ MODEL_FORMAT_MODE_TABLE,
+} ModelFormatMode;
+
+/** Enumeration of inst_format modes (how to print models from get-model command). */
+typedef enum {
+ /** default mode (print expressions in the output language format) */
+ INST_FORMAT_MODE_DEFAULT,
+ /** print as SZS proof */
+ INST_FORMAT_MODE_SZS,
+} InstFormatMode;
+
+std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, InstFormatMode mode) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PRINTER__MODEL_FORMAT_H */
module PRINTER "printer/options.h" Printing
-option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::printer::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "printer/model_format_mode.h" :handler-include "printer/options_handlers.h"
+option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::printer::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "printer/modes.h" :handler-include "printer/options_handlers.h"
print format mode for models, see --model-format=help
+option instFormatMode --inst-format=MODE InstFormatMode :handler CVC4::printer::stringToInstFormatMode :default INST_FORMAT_MODE_DEFAULT :read-write :include "printer/modes.h" :handler-include "printer/options_handlers.h"
+ print format mode for instantiations, see --inst-format=help
+
endmodule
#ifndef __CVC4__PRINTER__OPTIONS_HANDLERS_H
#define __CVC4__PRINTER__OPTIONS_HANDLERS_H
-#include "printer/model_format_mode.h"
+#include "printer/modes.h"
namespace CVC4 {
namespace printer {
+ Print functional expressions over finite domains in a table format.\n\
";
+static const std::string instFormatHelp = "\
+Inst format modes currently supported by the --model-format option:\n\
+\n\
+default \n\
++ Print instantiations as a list in the output language format.\n\
+\n\
+szs\n\
++ Print instantiations as SZS compliant proof.\n\
+";
+
inline ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
if(optarg == "default") {
return MODEL_FORMAT_MODE_DEFAULT;
}
}
+inline InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ if(optarg == "default") {
+ return INST_FORMAT_MODE_DEFAULT;
+ } else if(optarg == "szs") {
+ return INST_FORMAT_MODE_SZS;
+ } else if(optarg == "help") {
+ puts(instFormatHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(std::string("unknown option for --inst-format: `") +
+ optarg + "'. Try --inst-format help.");
+ }
+}
}/* CVC4::printer namespace */
}/* CVC4 namespace */
#include "theory/quantifiers/options.h"
#include "theory/datatypes/options.h"
#include "theory/strings/theory_strings_preprocess.h"
+#include "printer/options.h"
using namespace std;
using namespace CVC4;
Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl;
vector< TypeNode > fvTypes;
vector< TNode > fvs;
- d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ) );
+ d_assertionsToPreprocess[i] = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
if( prev!=d_assertionsToPreprocess[i] ){
+ d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl;
Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl;
}
#endif /* CVC4_PROOF */
}
-void SmtEngine::printInstantiations() {
- //TODO
+void SmtEngine::printInstantiations( std::ostream& out ) {
+ //if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
+ out << "% SZS CNF output start CNFRefutation for " << d_filename.c_str() << std::endl;
+ //}
+ if( d_theoryEngine ){
+ d_theoryEngine->printInstantiations( out );
+ }
+ //if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
+ out << "% SZS CNF output end CNFRefutation for " << d_filename.c_str() << std::endl;
+ //}
}
vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
/**
* Print all instantiations made by the quantifiers module.
*/
- void printInstantiations();
+ void printInstantiations( std::ostream& out );
/**
* Get the current set of assertions. Only permitted if the
}\r
}\r
\r
-void AbsDef::simplify( FirstOrderModelAbs * m, TNode n, unsigned depth ) {\r
+void AbsDef::simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth ) {\r
if( d_value==val_none && !d_def.empty() ){\r
//process the default\r
std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default );\r
Assert( defd!=d_def.end() );\r
unsigned newDef = d_default;\r
std::vector< unsigned > to_erase;\r
- defd->second.simplify( m, n, depth+1 );\r
+ defd->second.simplify( m, q, n, depth+1 );\r
int defVal = defd->second.d_value;\r
bool isConstant = ( defVal!=val_none );\r
//process each child\r
for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){\r
if( it->first!=d_default ){\r
- it->second.simplify( m, n, depth+1 );\r
+ it->second.simplify( m, q, n, depth+1 );\r
if( it->second.d_value==defVal && it->second.d_value!=val_none ){\r
newDef = newDef | it->first;\r
to_erase.push_back( it->first );\r
d_def.erase( d_default );\r
//set new default\r
d_default = newDef;\r
- d_def[d_default].construct_def_entry( m, n, defVal, depth+1 );\r
+ d_def[d_default].construct_def_entry( m, q, n, defVal, depth+1 );\r
//erase redundant entries\r
for( unsigned i=0; i<to_erase.size(); i++ ){\r
d_def.erase( to_erase[i] );\r
for( unsigned i=0; i<dSize; i++ ){\r
Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");\r
}\r
+ //Trace(c) << "(";\r
+ //for( unsigned i=0; i<32; i++ ){\r
+ // Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");\r
+ //}\r
+ //Trace(c) << ")";\r
}\r
\r
void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth ) const{\r
}\r
}\r
\r
-void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth ) {\r
+void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth ) {\r
d_value = v;\r
if( depth<n.getNumChildren() ){\r
- unsigned dom = m->d_domain[n[depth].getType()];\r
- d_def[dom].construct_def_entry( m, n, v, depth+1 );\r
+ TypeNode tn = q.isNull() ? n[depth].getType() : m->getVariable( q, depth ).getType();\r
+ unsigned dom = m->d_domain[tn] ;\r
+ d_def[dom].construct_def_entry( m, q, n, v, depth+1 );\r
d_default = dom;\r
}\r
}\r
for( std::map< unsigned, int >::iterator it = bchildren.begin(); it !=bchildren.end(); ++it ){\r
if( ( it->second==0 && n.getKind()==AND ) ||\r
( it->second==1 && n.getKind()==OR ) ){\r
- construct_def_entry( m, q[0], it->second );\r
+ construct_def_entry( m, q, q[0], it->second );\r
return true;\r
}\r
}\r
return (n & (n - 1))==0;\r
}\r
\r
-unsigned AbsDef::getId( unsigned n, unsigned start ) {\r
+unsigned AbsDef::getId( unsigned n, unsigned start, unsigned end ) {\r
Assert( n!=0 );\r
while( (n & ( 1 << start )) == 0 ){\r
start++;\r
- if( start==32 ){\r
+ if( start==end ){\r
return start;\r
}\r
}\r
Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl;\r
it->second->debugPrint("ambqi-model-debug", fm, fapps[0] );\r
Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl;\r
- it->second->simplify( fm, fapps[0] );\r
+ it->second->simplify( fm, TNode::null(), fapps[0] );\r
Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl;\r
it->second->debugPrint("ambqi-model", fm, fapps[0] );\r
\r
\r
//do exhaustive instantiation\r
bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {\r
- Trace("ambqi-check") << "exhaustive instantiation " << q << " " << effort << std::endl;\r
+ Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl;\r
if (effort==0) {\r
FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs();\r
bool quantValid = true;\r
}\r
}\r
if( quantValid ){\r
+ Trace("ambqi-check") << "Compute interpretation..." << std::endl;\r
AbsDef ad;\r
doCheck( fma, q, ad, q[1] );\r
//now process entries\r
Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl;\r
ad.debugPrint( "ambqi-inst", fma, q[0] );\r
Trace("ambqi-inst") << std::endl;\r
+ Trace("ambqi-check") << "Add instantiations..." << std::endl;\r
int lem = 0;\r
quantValid = ad.addInstantiations( fma, d_qe, q, lem );\r
Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl;\r
}\r
Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl;\r
ad.debugPrint("ambqi-check-try", m, q[0] );\r
- ad.simplify( m, q[0] );\r
+ ad.simplify( m, q, q[0] );\r
Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl;\r
ad.debugPrint("ambqi-check-debug", m, q[0] );\r
Trace("ambqi-check-debug") << std::endl;\r
std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,\r
std::vector< unsigned >& entry, std::vector< bool >& entry_def );\r
void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 );\r
- void construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth = 0 );\r
+ void construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth = 0 );\r
void apply_ucompose( FirstOrderModelAbs * m, TNode q,\r
std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms,\r
std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth = 0 );\r
void construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth = 0 );\r
void debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const;\r
void debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth = 0 ) const;\r
- void simplify( FirstOrderModelAbs * m, TNode q, unsigned depth = 0 );\r
+ void simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth = 0 );\r
int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){\r
std::vector< Node > terms;\r
terms.resize( q[0].getNumChildren() );\r
void negate();\r
Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 );\r
static bool isSimple( unsigned n );\r
- static unsigned getId( unsigned n, unsigned start=0 );\r
+ static unsigned getId( unsigned n, unsigned start=0, unsigned end=32 );\r
Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args );\r
Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 );\r
//for debugging\r
if (!d_rep_set.hasType(tn)) {
Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
- d_rep_set.add(mbt);
+ Trace("fmc-model-debug") << "Add to representative set..." << std::endl;
+ d_rep_set.add(tn, mbt);
}else if( d_rep_set.d_type_reps[tn].size()==0 ){
Message() << "empty reps" << std::endl;
exit(0);
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( n.getKind()==EQUAL && n[i].getKind()==BOUND_VARIABLE ){
int v = getVariableId( q, n[i] );
- Assert( v>=0 && v<q.getNumChildren() );
+ Assert( v>=0 && v<(int)q[0].getNumChildren() );
eq_vars[v] = true;
}
collectEqVars( q, n[i], eq_vars );
return true;
}
}
- if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !c[index].getType().isInteger() ){
+ if( c[index].getType().isSort() ){
//for star: check if all children are defined and have generalizations
if( c[index]==st ){ ///options::fmfFmcCoverSimplify()
//check if all children exist and are complete
}else{
mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);
}
+ Trace("fmc") << "Get used rep for " << mbn << std::endl;
Node mbnr = fm->getUsedRepresentative( mbn );
+ Trace("fmc") << "...got " << mbnr << std::endl;
fm->d_model_basis_rep[tn] = mbnr;
Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl;
}
}
}
-void InstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const {
+void InstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const {
if( terms.size()==q[0].getNumChildren() ){
- Trace(c) << " ( ";
+ out << " ( ";
for( unsigned i=0; i<terms.size(); i++ ){
- if( i>0 ) Trace(c) << ", ";
- Trace(c) << terms[i];
+ if( i>0 ) out << ", ";
+ //out << terms[i];
}
- Trace(c) << " )" << std::endl;
+ out << " )" << std::endl;
}else{
for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
terms.push_back( it->first );
- it->second.print( c, q, terms );
+ it->second.print( out, q, terms );
terms.pop_back();
}
}
}
}
-void CDInstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const{
+void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const{
if( d_valid.get() ){
if( terms.size()==q[0].getNumChildren() ){
- Trace(c) << " ( ";
+ out << " ( ";
for( unsigned i=0; i<terms.size(); i++ ){
- if( i>0 ) Trace(c) << ", ";
- Trace(c) << terms[i];
+ if( i>0 ) out << ", ";
+ //out << terms[i];
}
- Trace(c) << " )" << std::endl;
+ out << " )" << std::endl;
}else{
for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
terms.push_back( it->first );
- it->second->print( c, q, terms );
+ it->second->print( out, q, terms );
terms.pop_back();
}
}
/** the data */
std::map< Node, InstMatchTrie > d_data;
private:
- void print( const char * c, Node q, std::vector< Node >& terms ) const;
+ void print( std::ostream& out, Node q, std::vector< Node >& terms ) const;
public:
InstMatchTrie(){}
~InstMatchTrie(){}
}
bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
- void print( const char * c, Node q ) const{
+ void print( std::ostream& out, Node q ) const{
std::vector< Node > terms;
- print( c, q, terms );
+ print( out, q, terms );
}
};/* class InstMatchTrie */
/** is valid */
context::CDO< bool > d_valid;
private:
- void print( const char * c, Node q, std::vector< Node >& terms ) const;
+ void print( std::ostream& out, Node q, std::vector< Node >& terms ) const;
public:
CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
~CDInstMatchTrie(){}
}
bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
bool modInst = false, int index = 0, bool onlyExist = false );
- void print( const char * c, Node q ) const{
+ void print( std::ostream& out, Node q ) const{
std::vector< Node > terms;
- print( c, q, terms );
+ print( out, q, terms );
}
};/* class CDInstMatchTrie */
}
++(d_statistics.d_instantiation_rounds);
bool quantActive = false;
- Debug("quantifiers") << "quantifiers: check: asserted quantifiers size"
+ Debug("quantifiers") << "quantifiers: check: asserted quantifiers size="
<< d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
}
}
-void QuantifiersEngine::printInstantiations( const char * c ) {
- if( options::incrementalSolving() ){
- for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
- Trace(c) << "Instantiations of " << it->first << " : " << std::endl;
- it->second->print( c, it->first );
- }
- }else{
+void QuantifiersEngine::printInstantiations( std::ostream& out ) {
+ //Trace("ajr-temp") << "QE print inst." << std::endl;
+ //if( options::incrementalSolving() ){
+ // for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
+ // out << "Instantiations of " << it->first << " : " << std::endl;
+ // it->second->print( out, it->first );
+ // }
+ //}else{
for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
- Trace(c) << "Instantiations of " << it->first << " : " << std::endl;
- it->second.print( c, it->first );
+ out << "Instantiations of " << it->first << " : " << std::endl;
+ it->second.print( out, it->first );
+ out << std::endl;
}
- }
+ //}
}
QuantifiersEngine::Statistics::Statistics():
eq::EqualityEngine* getMasterEqualityEngine() ;
public:
/** print instantiations */
- void printInstantiations( const char * c );
+ void printInstantiations( std::ostream& out );
/** statistics class */
class Statistics {
public:
}
}
-void RepSet::add( Node n ){
- TypeNode t = n.getType();
- d_tmap[ n ] = (int)d_type_reps[t].size();
- d_type_reps[t].push_back( n );
+void RepSet::add( TypeNode tn, Node n ){
+ d_tmap[ n ] = (int)d_type_reps[tn].size();
+ Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
+ d_type_reps[tn].push_back( n );
}
int RepSet::getIndexFor( Node n ) const {
while( !te.isFinished() ){
Node n = *te;
if( std::find( d_type_reps[t].begin(), d_type_reps[t].end(), n )==d_type_reps[t].end() ){
- add( n );
+ add( t, n );
}
++te;
}
if( !d_rep_set->hasType( tn ) ){
Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" );
Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
- d_rep_set->add( var );
+ d_rep_set->add( tn, var );
}
}else if( tn.isInteger() ){
bool inc = false;
/** get cardinality for type */
int getNumRepresentatives( TypeNode tn ) const;
/** add representative for type */
- void add( Node n );
+ void add( TypeNode tn, Node n );
/** returns index in d_type_reps for node n */
int getIndexFor( Node n ) const;
/** complete all values */
return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
}
+void TheoryEngine::printInstantiations( std::ostream& out ) {
+ if( d_quantEngine ){
+ d_quantEngine->printInstantiations( out );
+ }
+}
+
static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
std::set<TNode> all;
*/
Node getModelValue(TNode var);
+ /**
+ * Print all instantiations made by the quantifiers module.
+ */
+ void printInstantiations( std::ostream& out );
+
/**
* Forwards an entailment check according to the given theoryOfMode.
* See theory.h for documentation on entailmentCheck().
std::map< Node, Node >::iterator itMap;
for (itMap = constantReps.begin(); itMap != constantReps.end(); ++itMap) {
tm->d_reps[itMap->first] = itMap->second;
- tm->d_rep_set.add(itMap->second);
+ tm->d_rep_set.add(itMap->second.getType(), itMap->second);
}
if (!fullModel) {
// Make sure every EC has a rep
for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) {
tm->d_reps[itMap->first] = itMap->second;
- tm->d_rep_set.add(itMap->second);
+ tm->d_rep_set.add(itMap->second.getType(), itMap->second);
}
for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
set<Node>& noRepSet = TypeSet::getSet(it);
set<Node>::iterator i;
for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
tm->d_reps[*i] = *i;
- tm->d_rep_set.add(*i);
+ tm->d_rep_set.add((*i).getType(), *i);
}
}
}
#include "util/sort_inference.h"
#include "theory/uf/options.h"
#include "smt/options.h"
-//#include "theory/rewriter.h"
+#include "theory/rewriter.h"
using namespace CVC4;
using namespace std;
std::map< Node, Node > var_bound;
assertions[i] = simplify( assertions[i], var_bound );
if( prev!=assertions[i] ){
+ assertions[i] = theory::Rewriter::rewrite( assertions[i] );
rewritten = true;
Trace("sort-inference-rewrite") << prev << std::endl;
Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl;
Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl;
Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 );
Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 );
- return NodeManager::currentNM()->mkNode( kind::FORALL,
- NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ),
- NodeManager::currentNM()->mkNode( kind::IMPLIES,
- NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ),
- v1.eqNode( v2 ) ) );
+ Node ret = NodeManager::currentNM()->mkNode( kind::FORALL,
+ NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ),
+ NodeManager::currentNM()->mkNode( kind::OR,
+ NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ).negate(),
+ v1.eqNode( v2 ) ) );
+ ret = theory::Rewriter::rewrite( ret );
+ return ret;
}
int SortInference::getSortId( Node n ) {
projects / cvc5.git / commitdiff