summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Makefile.am4
-rw-r--r--src/expr/command.cpp6
-rw-r--r--src/expr/command.h1
-rw-r--r--src/main/command_executor.cpp2
-rw-r--r--src/printer/modes.cpp (renamed from src/printer/model_format_mode.cpp)18
-rw-r--r--src/printer/modes.h (renamed from src/printer/model_format_mode.h)15
-rw-r--r--src/printer/options5
-rw-r--r--src/printer/options_handlers.h25
-rw-r--r--src/smt/smt_engine.cpp16
-rw-r--r--src/smt/smt_engine.h2
-rwxr-xr-xsrc/theory/quantifiers/ambqi_builder.cpp34
-rwxr-xr-xsrc/theory/quantifiers/ambqi_builder.h6
-rw-r--r--src/theory/quantifiers/first_order_model.cpp5
-rw-r--r--src/theory/quantifiers/full_model_check.cpp4
-rw-r--r--src/theory/quantifiers/inst_match.cpp24
-rw-r--r--src/theory/quantifiers/inst_match.h12
-rw-r--r--src/theory/quantifiers/instantiation_engine.cpp2
-rw-r--r--src/theory/quantifiers_engine.cpp22
-rw-r--r--src/theory/quantifiers_engine.h2
-rw-r--r--src/theory/rep_set.cpp12
-rw-r--r--src/theory/rep_set.h2
-rw-r--r--src/theory/theory_engine.cpp6
-rw-r--r--src/theory/theory_engine.h5
-rw-r--r--src/theory/theory_model.cpp6
-rw-r--r--src/util/sort_inference.cpp15
25 files changed, 170 insertions, 81 deletions
diff --git a/src/Makefile.am b/src/Makefile.am
index 573181ccf..539afc781 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -67,8 +67,8 @@ libcvc4_la_SOURCES = \
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 \
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 34cdd2e30..9f502c2ea 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1055,7 +1055,7 @@ GetInstantiationsCommand::GetInstantiationsCommand() throw() {
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());
@@ -1070,19 +1070,21 @@ void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity
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;
}
diff --git a/src/expr/command.h b/src/expr/command.h
index ad9cd1aa7..ed6be86de 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -578,6 +578,7 @@ public:
class CVC4_PUBLIC GetInstantiationsCommand : public Command {
protected:
//Instantiations* d_result;
+ SmtEngine* d_smtEngine;
public:
GetInstantiationsCommand() throw();
~GetInstantiationsCommand() throw() {}
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 4dc49ee53..a1410d910 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -101,7 +101,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
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);
}
diff --git a/src/printer/model_format_mode.cpp b/src/printer/modes.cpp
index a8f946a8d..4f7242318 100644
--- a/src/printer/model_format_mode.cpp
+++ b/src/printer/modes.cpp
@@ -1,5 +1,5 @@
/********************* */
-/*! \file model_format_mode.cpp
+/*! \file modes.cpp
** \verbatim
** Original author: Morgan Deters
** Major contributors: Andrew Reynolds
@@ -15,7 +15,7 @@
** \todo document this file
**/
-#include "printer/model_format_mode.h"
+#include "printer/modes.h"
namespace CVC4 {
@@ -34,4 +34,18 @@ std::ostream& operator<<(std::ostream& out, ModelFormatMode 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 */
diff --git a/src/printer/model_format_mode.h b/src/printer/modes.h
index c729c6e5d..9673f791c 100644
--- a/src/printer/model_format_mode.h
+++ b/src/printer/modes.h
@@ -1,5 +1,5 @@
/********************* */
-/*! \file model_format_mode.h
+/*! \file modes.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: Andrew Reynolds
@@ -17,8 +17,8 @@
#include "cvc4_public.h"
-#ifndef __CVC4__PRINTER__MODEL_FORMAT_MODE_H
-#define __CVC4__PRINTER__MODEL_FORMAT_MODE_H
+#ifndef __CVC4__PRINTER__MODES_H
+#define __CVC4__PRINTER__MODES_H
#include <iostream>
@@ -32,7 +32,16 @@ typedef enum {
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 */
diff --git a/src/printer/options b/src/printer/options
index 7e1b67986..4daa9c77d 100644
--- a/src/printer/options
+++ b/src/printer/options
@@ -5,7 +5,10 @@
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
diff --git a/src/printer/options_handlers.h b/src/printer/options_handlers.h
index 97d0e64c9..2a89a8d38 100644
--- a/src/printer/options_handlers.h
+++ b/src/printer/options_handlers.h
@@ -19,7 +19,7 @@
#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 {
@@ -34,6 +34,16 @@ table\n\
+ 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;
@@ -48,6 +58,19 @@ inline ModelFormatMode stringToModelFormatMode(std::string option, std::string o
}
}
+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 */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5d6a913b0..0604988d3 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -86,6 +86,7 @@
#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;
@@ -2898,8 +2899,9 @@ void SmtEnginePrivate::processAssertions() {
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;
}
@@ -3792,8 +3794,16 @@ Proof* SmtEngine::getProof() throw(ModalException) {
#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) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 88ba55b45..4b981f614 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -500,7 +500,7 @@ public:
/**
* 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
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index c6a5f4227..e86a96a8f 100755
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -73,20 +73,20 @@ void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps
}
}
-void AbsDef::simplify( FirstOrderModelAbs * m, TNode n, unsigned depth ) {
+void AbsDef::simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth ) {
if( d_value==val_none && !d_def.empty() ){
//process the default
std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default );
Assert( defd!=d_def.end() );
unsigned newDef = d_default;
std::vector< unsigned > to_erase;
- defd->second.simplify( m, n, depth+1 );
+ defd->second.simplify( m, q, n, depth+1 );
int defVal = defd->second.d_value;
bool isConstant = ( defVal!=val_none );
//process each child
for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
if( it->first!=d_default ){
- it->second.simplify( m, n, depth+1 );
+ it->second.simplify( m, q, n, depth+1 );
if( it->second.d_value==defVal && it->second.d_value!=val_none ){
newDef = newDef | it->first;
to_erase.push_back( it->first );
@@ -101,7 +101,7 @@ void AbsDef::simplify( FirstOrderModelAbs * m, TNode n, unsigned depth ) {
d_def.erase( d_default );
//set new default
d_default = newDef;
- d_def[d_default].construct_def_entry( m, n, defVal, depth+1 );
+ d_def[d_default].construct_def_entry( m, q, n, defVal, depth+1 );
//erase redundant entries
for( unsigned i=0; i<to_erase.size(); i++ ){
d_def.erase( to_erase[i] );
@@ -120,6 +120,11 @@ void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const{
for( unsigned i=0; i<dSize; i++ ){
Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
}
+ //Trace(c) << "(";
+ //for( unsigned i=0; i<32; i++ ){
+ // Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
+ //}
+ //Trace(c) << ")";
}
void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth ) const{
@@ -257,11 +262,12 @@ void AbsDef::construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector<
}
}
-void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth ) {
+void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth ) {
d_value = v;
if( depth<n.getNumChildren() ){
- unsigned dom = m->d_domain[n[depth].getType()];
- d_def[dom].construct_def_entry( m, n, v, depth+1 );
+ TypeNode tn = q.isNull() ? n[depth].getType() : m->getVariable( q, depth ).getType();
+ unsigned dom = m->d_domain[tn] ;
+ d_def[dom].construct_def_entry( m, q, n, v, depth+1 );
d_default = dom;
}
}
@@ -556,7 +562,7 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
for( std::map< unsigned, int >::iterator it = bchildren.begin(); it !=bchildren.end(); ++it ){
if( ( it->second==0 && n.getKind()==AND ) ||
( it->second==1 && n.getKind()==OR ) ){
- construct_def_entry( m, q[0], it->second );
+ construct_def_entry( m, q, q[0], it->second );
return true;
}
}
@@ -654,11 +660,11 @@ bool AbsDef::isSimple( unsigned n ) {
return (n & (n - 1))==0;
}
-unsigned AbsDef::getId( unsigned n, unsigned start ) {
+unsigned AbsDef::getId( unsigned n, unsigned start, unsigned end ) {
Assert( n!=0 );
while( (n & ( 1 << start )) == 0 ){
start++;
- if( start==32 ){
+ if( start==end ){
return start;
}
}
@@ -808,7 +814,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl;
it->second->debugPrint("ambqi-model-debug", fm, fapps[0] );
Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl;
- it->second->simplify( fm, fapps[0] );
+ it->second->simplify( fm, TNode::null(), fapps[0] );
Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl;
it->second->debugPrint("ambqi-model", fm, fapps[0] );
@@ -831,7 +837,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
//do exhaustive instantiation
bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
- Trace("ambqi-check") << "exhaustive instantiation " << q << " " << effort << std::endl;
+ Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl;
if (effort==0) {
FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs();
bool quantValid = true;
@@ -843,6 +849,7 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in
}
}
if( quantValid ){
+ Trace("ambqi-check") << "Compute interpretation..." << std::endl;
AbsDef ad;
doCheck( fma, q, ad, q[1] );
//now process entries
@@ -850,6 +857,7 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in
Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl;
ad.debugPrint( "ambqi-inst", fma, q[0] );
Trace("ambqi-inst") << std::endl;
+ Trace("ambqi-check") << "Add instantiations..." << std::endl;
int lem = 0;
quantValid = ad.addInstantiations( fma, d_qe, q, lem );
Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl;
@@ -919,7 +927,7 @@ bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNod
}
Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl;
ad.debugPrint("ambqi-check-try", m, q[0] );
- ad.simplify( m, q[0] );
+ ad.simplify( m, q, q[0] );
Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl;
ad.debugPrint("ambqi-check-debug", m, q[0] );
Trace("ambqi-check-debug") << std::endl;
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h
index 784fa5093..349073cb4 100755
--- a/src/theory/quantifiers/ambqi_builder.h
+++ b/src/theory/quantifiers/ambqi_builder.h
@@ -36,7 +36,7 @@ private:
std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
std::vector< unsigned >& entry, std::vector< bool >& entry_def );
void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 );
- void construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth = 0 );
+ void construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth = 0 );
void apply_ucompose( FirstOrderModelAbs * m, TNode q,
std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms,
std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth = 0 );
@@ -59,7 +59,7 @@ public:
void construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth = 0 );
void debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const;
void debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth = 0 ) const;
- void simplify( FirstOrderModelAbs * m, TNode q, unsigned depth = 0 );
+ void simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth = 0 );
int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){
std::vector< Node > terms;
terms.resize( q[0].getNumChildren() );
@@ -73,7 +73,7 @@ public:
void negate();
Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 );
static bool isSimple( unsigned n );
- static unsigned getId( unsigned n, unsigned start=0 );
+ static unsigned getId( unsigned n, unsigned start=0, unsigned end=32 );
Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args );
Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 );
//for debugging
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index e4b588ac1..3edf97467 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -102,7 +102,8 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
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);
@@ -986,7 +987,7 @@ void FirstOrderModelAbs::collectEqVars( TNode q, TNode n, std::map< int, bool >&
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 );
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 0f3e53827..63df56392 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -61,7 +61,7 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
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
@@ -537,7 +537,9 @@ void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){
}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;
}
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 096d0cab2..703a44d03 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -198,18 +198,18 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
}
}
-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();
}
}
@@ -282,19 +282,19 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
}
}
-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();
}
}
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 2cf63210b..accd3baed 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -101,7 +101,7 @@ public:
/** 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(){}
@@ -128,9 +128,9 @@ public:
}
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 */
@@ -142,7 +142,7 @@ public:
/** 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(){}
@@ -169,9 +169,9 @@ public:
}
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 */
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 06858cf92..123dc02b6 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -210,7 +210,7 @@ void InstantiationEngine::check( Theory::Effort e ){
}
++(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 );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8fecc6ee0..a16f46ace 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -623,18 +623,20 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
}
}
-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():
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 7a899db0c..fa3c66f4f 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -236,7 +236,7 @@ public:
eq::EqualityEngine* getMasterEqualityEngine() ;
public:
/** print instantiations */
- void printInstantiations( const char * c );
+ void printInstantiations( std::ostream& out );
/** statistics class */
class Statistics {
public:
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 2e8eb51b1..7dd8d02f6 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -37,10 +37,10 @@ int RepSet::getNumRepresentatives( TypeNode tn ) const{
}
}
-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 {
@@ -59,7 +59,7 @@ void RepSet::complete( TypeNode t ){
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;
}
@@ -143,7 +143,7 @@ bool RepSetIterator::initialize(){
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;
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index a619915ee..c72e46e76 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -40,7 +40,7 @@ public:
/** 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 */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 18968e897..c63df83ee 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1179,6 +1179,12 @@ Node TheoryEngine::getModelValue(TNode var) {
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;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0495a866b..615598e44 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -759,6 +759,11 @@ public:
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().
*/
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 7187a373f..203f116bb 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -737,7 +737,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
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) {
@@ -745,14 +745,14 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool 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);
}
}
}
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index ce12b59f1..b38ed7d63 100644
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -22,7 +22,7 @@
#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;
@@ -172,6 +172,7 @@ bool SortInference::simplify( std::vector< Node >& assertions ){
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;
@@ -626,11 +627,13 @@ Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) {
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 ) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback