(this commit was certified error- and warning-free by the test-and-commit script.)
check_theory_seen
}
-function instantiator {
- # instantiator class header
- lineno=${BASH_LINENO[0]}
- check_theory_seen
-}
-
function properties {
# properties prop*
lineno=${BASH_LINENO[0]}
"
}
-function instantiator {
- # instantiator class header
- lineno=${BASH_LINENO[0]}
- check_theory_seen
-}
-
function properties {
# rewriter class header
lineno=${BASH_LINENO[0]}
// #include \"theory/$b/$2\""
}
-function instantiator {
- # instantiator class header
- lineno=${BASH_LINENO[0]}
- check_theory_seen
-}
-
function properties {
# properties prop*
lineno=${BASH_LINENO[0]}
nodist_libtheory_la_SOURCES = \
rewriter_tables.h \
- instantiator_tables.cpp \
theory_traits.h \
type_enumerator.cpp
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
`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
namespace theory {
namespace datatypes {
-class InstantiatorTheoryDatatypes;
class EqualityQueryTheory;
class TheoryDatatypes : public Theory {
- friend class InstantiatorTheoryDatatypes;
friend class EqualityQueryTheory;
private:
typedef context::CDChunkList<Node> NodeList;
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-#!/bin/bash
-#
-# mkinstantiator
-# Morgan Deters <mdeters@cs.nyu.edu> 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 <<EOF
-/********************* */
-/** instantiator_tables.h
- **
- ** Copyright $copyright The AcSys Group, New York University, and as below.
- **
- ** This header file automatically generated by:
- **
- ** $0 $@
- **
- ** for the CVC4 project.
- **/
-
-EOF
-
-me=$(basename "$0")
-
-template=$1; shift
-
-instantiator_includes=
-instantiator_class=
-theory_id=
-theory_class=
-theory_header=
-
-make_instantiator_cases=
-instantiator=
-
-seen_theory=false
-seen_theory_builtin=false
-
-function theory {
- # theory id T header
-
- lineno=${BASH_LINENO[0]}
-
- if $seen_theory; then
- echo "$kf:$lineno: theory declaration can only appear once" >&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"
theory_id="$1"
}
-function instantiator {
- # instantiator class header
- lineno=${BASH_LINENO[0]}
- check_theory_seen
-}
-
function properties {
# properties prop*
lineno=${BASH_LINENO[0]}
rewriter_class=
rewriter_header=
-instantiator_class=void
-instantiator_header=
-
theory_id=
theory_class=
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};
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]}
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)) {
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) {
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;
}
}
}/* ostream& operator<<(ostream&, Theory::Effort) */
Theory::~Theory() {
- if(d_inst != NULL) {
- delete d_inst;
- d_inst = NULL;
- }
-
StatisticsRegistry::unregisterStat(&d_computeCareGraphTime);
}
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<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
std::hash_set<TNode, TNodeHashFunction> currentlyShared;
for(shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i){
namespace theory {
-class Instantiator;
class QuantifiersEngine;
class TheoryModel;
*/
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;
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:
/**
, 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)
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.
*/
}
-/** 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!" );
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;
}
};/* struct NodeTheoryPairHashFunction */
namespace theory {
- class Instantiator;
class TheoryModel;
class TheoryEngineModelBuilder;
namespace uf {
class UfTermDb;
-class InstantiatorTheoryUf;
class StrongSolverTheoryUf;
class TheoryUF : public Theory {
- friend class InstantiatorTheoryUf;
friend class StrongSolverTheoryUf;
public:
projects / cvc5.git / commitdiff