From e820acb9e220389e9a7e23bcffd97f1d0354f612 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 1 Dec 2012 15:13:58 +0000 Subject: [PATCH] remove instantiator framework (this commit was certified error- and warning-free by the test-and-commit script.) --- src/expr/mkexpr | 6 - src/expr/mkkind | 6 - src/expr/mkmetakind | 6 - src/theory/Makefile.am | 13 - src/theory/datatypes/theory_datatypes.h | 2 - src/theory/instantiator_tables_template.cpp | 38 --- src/theory/mkinstantiator | 254 -------------------- src/theory/mkrewriter | 6 - src/theory/mktheorytraits | 16 -- src/theory/term_registration_visitor.cpp | 9 - src/theory/theory.cpp | 72 ------ src/theory/theory.h | 82 ------- src/theory/theory_engine.h | 1 - src/theory/uf/theory_uf.h | 2 - 14 files changed, 513 deletions(-) delete mode 100644 src/theory/instantiator_tables_template.cpp delete mode 100755 src/theory/mkinstantiator diff --git a/src/expr/mkexpr b/src/expr/mkexpr index ec8d0d12f..5134d561e 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -98,12 +98,6 @@ function rewriter { check_theory_seen } -function instantiator { - # instantiator class header - lineno=${BASH_LINENO[0]} - check_theory_seen -} - function properties { # properties prop* lineno=${BASH_LINENO[0]} diff --git a/src/expr/mkkind b/src/expr/mkkind index 88c28d4b9..786d6187b 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -105,12 +105,6 @@ function theory { " } -function instantiator { - # instantiator class header - lineno=${BASH_LINENO[0]} - check_theory_seen -} - function properties { # rewriter class header lineno=${BASH_LINENO[0]} diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 4582bfeda..47ffc77f9 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -80,12 +80,6 @@ function theory { // #include \"theory/$b/$2\"" } -function instantiator { - # instantiator class header - lineno=${BASH_LINENO[0]} - check_theory_seen -} - function properties { # properties prop* lineno=${BASH_LINENO[0]} diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 1f0108581..1362b1f5c 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -45,7 +45,6 @@ libtheory_la_SOURCES = \ nodist_libtheory_la_SOURCES = \ rewriter_tables.h \ - instantiator_tables.cpp \ theory_traits.h \ type_enumerator.cpp @@ -64,23 +63,19 @@ EXTRA_DIST = \ logic_info.i \ options_handlers.h \ rewriter_tables_template.h \ - instantiator_tables_template.cpp \ theory_traits_template.h \ type_enumerator_template.cpp \ mktheorytraits \ mkrewriter \ - mkinstantiator \ Makefile.subdirs BUILT_SOURCES = \ rewriter_tables.h \ - instantiator_tables.cpp \ theory_traits.h \ type_enumerator.cpp CLEANFILES = \ rewriter_tables.h \ - instantiator_tables.cpp \ theory_traits.h \ type_enumerator.cpp @@ -94,14 +89,6 @@ rewriter_tables.h: rewriter_tables_template.h mkrewriter @top_builddir@/src/theo `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) -instantiator_tables.cpp: instantiator_tables_template.cpp mkinstantiator @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkinstantiator - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkinstantiator \ - $< \ - `cat @top_builddir@/src/theory/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - theory_traits.h: theory_traits_template.h mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mktheorytraits $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 4380eca58..90d82e255 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -34,11 +34,9 @@ namespace CVC4 { namespace theory { namespace datatypes { -class InstantiatorTheoryDatatypes; class EqualityQueryTheory; class TheoryDatatypes : public Theory { - friend class InstantiatorTheoryDatatypes; friend class EqualityQueryTheory; private: typedef context::CDChunkList NodeList; diff --git a/src/theory/instantiator_tables_template.cpp b/src/theory/instantiator_tables_template.cpp deleted file mode 100644 index bc038df63..000000000 --- a/src/theory/instantiator_tables_template.cpp +++ /dev/null @@ -1,38 +0,0 @@ -/********************* */ -/*! \file instantiator_tables_template.cpp - ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters - ** 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 Instantiator tables for quantifier-friendly theories - ** - ** This file contains template code for the instantiator tables that are - ** generated from the Theory kinds files. - **/ - -#include "context/context.h" -#include "theory/quantifiers_engine.h" - -${instantiator_includes} - -#line 24 "${template}" - -namespace CVC4 { -namespace theory { - -Instantiator* Theory::makeInstantiator(context::Context* c, theory::QuantifiersEngine* qe) { - switch(d_id) { -${make_instantiator_cases} -#line 32 "${template}" - default: - Unhandled(d_id); - } -} - -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ diff --git a/src/theory/mkinstantiator b/src/theory/mkinstantiator deleted file mode 100755 index 73fc6706d..000000000 --- a/src/theory/mkinstantiator +++ /dev/null @@ -1,254 +0,0 @@ -#!/bin/bash -# -# mkinstantiator -# Morgan Deters for CVC4 -# Copyright (c) 2010-2012 The CVC4 Project -# -# The purpose of this script is to create rewriter_tables.h from a template -# and a list of theory kinds. -# -# Invocation: -# -# mkinstantiator template-file theory-kind-files... -# -# Output is to standard out. -# - -copyright=2010-2012 - -cat <&2 - exit 1; - fi - - seen_theory=true - if [ "$1" = THEORY_BUILTIN ]; then - if $seen_theory_builtin; then - echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2 - exit 1 - fi - seen_theory_builtin=true - elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then - echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2 - exit 1 - elif ! expr "$2" : '\(::*\)' >/dev/null; then - echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2 - elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then - echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2 - fi - - theory_id="$1" - theory_class="$2" - theory_header="$3" - - instantiator_class= - instantiator=NULL -} - -function instantiator { - # instantiator class header - lineno=${BASH_LINENO[0]} - check_theory_seen - - if [ -n "$instantiator_class" ]; then - echo "$kf:$lineno: error: cannot have two \"instantiator\" directives" >&2 - exit 1 - fi - - instantiator_class="$1" - instantiator_header="$2" - - if [ -z "$instantiator_class" -o -z "$instantiator_header" ]; then - echo "$kf:$lineno: error: \"instantiator\" directive missing class or header argument" >&2 - exit 1 - fi - - instantiator_includes="${instantiator_includes}#include \"$theory_header\" -#line $lineno \"$kf\" -#include \"$instantiator_header\" -" - instantiator="new $instantiator_class(c, qe, static_cast< $theory_class* >(this))"; -} - -function properties { - # properties prop* - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -function endtheory { - # endtheory - lineno=${BASH_LINENO[0]} - check_theory_seen - seen_endtheory=true - - make_instantiator_cases="${make_instantiator_cases} -#line $lineno \"$kf\" - case $theory_id: - return $instantiator; -" -} - -function enumerator { - # enumerator KIND enumerator-class header - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -function typechecker { - # typechecker header - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -function typerule { - # typerule OPERATOR typechecking-class - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -function construle { - # construle OPERATOR isconst-checking-class - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -function rewriter { - # rewriter class header - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -function sort { - # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -function cardinality { - # cardinality TYPE cardinality-computer [header] - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -function well-founded { - # well-founded TYPE wellfoundedness-computer [header] - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -function variable { - # variable K ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -function operator { - # operator K #children ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -function parameterized { - # parameterized K1 K2 #children ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -function constant { - # constant K T Hasher header ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -function check_theory_seen { - if $seen_endtheory; then - echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2 - exit 1 - fi - if ! $seen_theory; then - echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 - exit 1 - fi -} - -function check_builtin_theory_seen { - if ! $seen_theory_builtin; then - echo "$me: warning: no declaration for the builtin theory found" >&2 - fi -} - -while [ $# -gt 0 ]; do - kf=$1 - seen_theory=false - seen_endtheory=false - b=$(basename $(dirname "$kf")) - source "$kf" - if ! $seen_theory; then - echo "$kf: error: no theory content found in file!" >&2 - exit 1 - fi - if ! $seen_endtheory; then - echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2 - exit 1 - fi - shift -done -check_builtin_theory_seen - -## output - -# generate warnings about incorrect #line annotations in templates -nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' | - awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2 - -text=$(cat "$template") -for var in \ - instantiator_includes \ - make_instantiator_cases \ - template \ - ; do - eval text="\${text//\\\$\\{$var\\}/\${$var}}" -done -error=`expr "$text" : '.*\${\([^}]*\)}.*'` -if [ -n "$error" ]; then - echo "$template:0: error: undefined replacement \${$error}" >&2 - exit 1 -fi -echo "$text" diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index 0d00b616c..88ac5b9fb 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -81,12 +81,6 @@ function theory { theory_id="$1" } -function instantiator { - # instantiator class header - lineno=${BASH_LINENO[0]} - check_theory_seen -} - function properties { # properties prop* lineno=${BASH_LINENO[0]} diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index c8ef23a78..a44d8e9c3 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -61,9 +61,6 @@ theory_parametric="false" rewriter_class= rewriter_header= -instantiator_class=void -instantiator_header= - theory_id= theory_class= @@ -135,7 +132,6 @@ template<> struct TheoryTraits<${theory_id}> { typedef ${theory_class} theory_class; typedef ${rewriter_class} rewriter_class; - typedef ${instantiator_class} instantiator_class; static const bool isStableInfinite = ${theory_stable_infinite}; static const bool isFinite = ${theory_finite}; @@ -240,18 +236,6 @@ function construle { check_theory_seen } -function instantiator { - # instantiator class header - lineno=${BASH_LINENO[0]} - check_theory_seen - - instantiator_class="$1" - instantiator_header="$2" - - theory_includes="${theory_includes}#include \"$2\" -" -} - function properties { # properties property* lineno=${BASH_LINENO[0]} diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index c32d6ff75..b41089b80 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -102,9 +102,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { d_visited[current] = visitedTheories; Theory* th = d_engine->theoryOf(currentTheoryId); th->preRegisterTerm(current); - if(th->getInstantiator() != NULL) { - th->getInstantiator()->preRegisterTerm(current); - } Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; } if (!Theory::setContains(parentTheoryId, visitedTheories)) { @@ -112,9 +109,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { d_visited[current] = visitedTheories; Theory* th = d_engine->theoryOf(parentTheoryId); th->preRegisterTerm(current); - if(th->getInstantiator() != NULL) { - th->getInstantiator()->preRegisterTerm(current); - } Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } if (useType) { @@ -124,9 +118,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { d_visited[current] = visitedTheories; Theory* th = d_engine->theoryOf(typeTheoryId); th->preRegisterTerm(current); - if(th->getInstantiator() != NULL) { - th->getInstantiator()->preRegisterTerm(current); - } Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } } diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index ea3902d59..f513b0d78 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -48,11 +48,6 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ }/* ostream& operator<<(ostream&, Theory::Effort) */ Theory::~Theory() { - if(d_inst != NULL) { - delete d_inst; - d_inst = NULL; - } - StatisticsRegistry::unregisterStat(&d_computeCareGraphTime); } @@ -174,73 +169,6 @@ void Theory::debugPrintFacts() const{ printFacts(DebugChannel.getStream()); } -Instantiator::Instantiator(context::Context* c, QuantifiersEngine* qe, Theory* th) : - d_quantEngine(qe), - d_th(th) { -} - -Instantiator::~Instantiator() { -} - -void Instantiator::resetInstantiationRound(Theory::Effort effort) { - /* - for(int i = 0; i < (int) d_instStrategies.size(); ++i) { - if(isActiveStrategy(d_instStrategies[i])) { - d_instStrategies[i]->processResetInstantiationRound(effort); - } - } - processResetInstantiationRound(effort); - */ -} - -int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) { - /* - if( getQuantifierActive(f) ) { - int status = process(f, effort, e ); - if(d_instStrategies.empty()) { - Debug("inst-engine-inst") << "There are no instantiation strategies allocated." << endl; - } else { - for(int i = 0; i < (int) d_instStrategies.size(); ++i) { - if(isActiveStrategy(d_instStrategies[i])) { - Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " process " << effort << endl; - //call the instantiation strategy's process method - int s_status = d_instStrategies[i]->process( f, effort, e ); - Debug("inst-engine-inst") << " -> status is " << s_status << endl; - InstStrategy::updateStatus(status, s_status); - } else { - Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " is not active." << endl; - } - } - } - return status; - } else { - Debug("inst-engine-inst") << "We have no constraints from this quantifier." << endl; - return InstStrategy::STATUS_SAT; - } - */ - return 0; -} - -//void Instantiator::doInstantiation(int effort) { -// d_status = InstStrategy::STATUS_SAT; -// for( int q = 0; q < d_quantEngine->getNumQuantifiers(); ++q ) { -// Node f = d_quantEngine->getQuantifier(q); -// if( d_quantEngine->getActive(f) && hasConstraintsFrom(f) ) { -// int d_quantStatus = process( f, effort ); -// InstStrategy::updateStatus( d_status, d_quantStatus ); -// for( int i = 0; i < (int)d_instStrategies.size(); ++i ) { -// if( isActiveStrategy( d_instStrategies[i] ) ) { -// Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " process " << effort << endl; -// //call the instantiation strategy's process method -// d_quantStatus = d_instStrategies[i]->process( f, effort ); -// Debug("inst-engine-inst") << " -> status is " << d_quantStatus << endl; -// InstStrategy::updateStatus( d_status, d_quantStatus ); -// } -// } -// } -// } -//} - std::hash_set Theory::currentlySharedTerms() const{ std::hash_set currentlyShared; for(shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i){ diff --git a/src/theory/theory.h b/src/theory/theory.h index 1f55a4b90..f317d4b92 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -46,7 +46,6 @@ class TheoryEngine; namespace theory { -class Instantiator; class QuantifiersEngine; class TheoryModel; @@ -192,12 +191,6 @@ private: */ QuantifiersEngine* d_quantEngine; - /** - * The instantiator for this theory, or NULL if quantifiers are not - * supported or not enabled. - */ - Instantiator* d_inst; - // === STATISTICS === /** time spent in theory combination */ TimerStat d_computeCareGraphTime; @@ -208,12 +201,6 @@ private: return ss.str(); } - /** - * Construct and return the instantiator for the given theory. - * If there is no instantiator class, NULL is returned. - */ - theory::Instantiator* makeInstantiator(context::Context* c, theory::QuantifiersEngine* qe); - protected: /** @@ -261,7 +248,6 @@ protected: , d_sharedTermsIndex(satContext, 0) , d_careGraph(0) , d_quantEngine(qe) - , d_inst(makeInstantiator(satContext, qe)) , d_computeCareGraphTime(statName(id, "computeCareGraphTime")) , d_sharedTerms(satContext) , d_out(&out) @@ -486,20 +472,6 @@ public: return d_quantEngine; } - /** - * Get the theory instantiator. - */ - Instantiator* getInstantiator() { - return d_inst; - } - - /** - * Get the theory instantiator (const version). - */ - const Instantiator* getInstantiator() const { - return d_inst; - } - /** * Pre-register a term. Done one time for a Node, ever. */ @@ -821,55 +793,6 @@ namespace eq{ } -/** instantiator class */ -class Instantiator { - friend class QuantifiersEngine; -protected: - /** reference to the quantifiers engine */ - QuantifiersEngine* d_quantEngine; - /** reference to the theory that it looks at */ - Theory* d_th; - /** reset instantiation round */ - virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; - /** process quantifier */ - virtual int process( Node f, Theory::Effort effort, int e ) = 0; -public: - Instantiator(context::Context* c, QuantifiersEngine* qe, Theory* th); - virtual ~Instantiator(); - - /** get quantifiers engine */ - QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } - /** get corresponding theory for this instantiator */ - Theory* getTheory() { return d_th; } - /** Pre-register a term. */ - virtual void preRegisterTerm( Node t ) { } - /** assertNode function, assertion was asserted to theory */ - virtual void assertNode( Node assertion ){} - /** identify */ - virtual std::string identify() const { return std::string("Unknown"); } - /** print debug information */ - virtual void debugPrint( const char* c ) {} -public: - /** reset instantiation round */ - void resetInstantiationRound( Theory::Effort effort ); - /** do instantiation method*/ - int doInstantiation( Node f, Theory::Effort effort, int e ); -public: - /** general queries about equality */ - virtual bool hasTerm( Node a ) { return false; } - virtual bool areEqual( Node a, Node b ) { return false; } - virtual bool areDisequal( Node a, Node b ) { return false; } - virtual Node getRepresentative( Node a ) { return a; } - virtual eq::EqualityEngine* getEqualityEngine() { return NULL; } - virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) {} -public: - /** A Creator of CandidateGenerator for classes (one element in each - equivalence class) and class (every element of one equivalence - class) */ - virtual rrinst::CandidateGenerator* getRRCanGenClasses(){ return NULL; }; - virtual rrinst::CandidateGenerator* getRRCanGenClass(){ return NULL; }; -};/* class Instantiator */ - inline Assertion Theory::get() { Assert( !done(), "Theory::get() called with assertion queue empty!" ); @@ -883,11 +806,6 @@ inline Assertion Theory::get() { Dump("state") << AssertCommand(fact.assertion.toExpr()); } - // if quantifiers are turned on and we have an instantiator, notify it - if(getLogicInfo().isQuantified() && getInstantiator() != NULL) { - getInstantiator()->assertNode(fact); - } - return fact; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 4a1ab4ca0..063943056 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -74,7 +74,6 @@ struct NodeTheoryPairHashFunction { };/* struct NodeTheoryPairHashFunction */ namespace theory { - class Instantiator; class TheoryModel; class TheoryEngineModelBuilder; diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 46a17a5e0..fe1fc5137 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -35,12 +35,10 @@ namespace theory { namespace uf { class UfTermDb; -class InstantiatorTheoryUf; class StrongSolverTheoryUf; class TheoryUF : public Theory { - friend class InstantiatorTheoryUf; friend class StrongSolverTheoryUf; public: -- 2.30.2