1 /********************* */ 2 /*! \file theory_idl.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Dejan Jovanovic, Mathias Preiner, Tim King 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief [[ Add one-line brief description here ]] 13 ** 14 ** [[ Add lengthier description here ]] 15 ** \todo document this file 16 **/ 17 18 #pragma once 19 20 #include "cvc4_private.h" 21 22 #include "theory/theory.h" 23 #include "theory/idl/idl_model.h" 24 #include "theory/idl/idl_assertion_db.h" 25 26 namespace CVC4 { 27 namespace theory { 28 namespace idl { 29 30 /** 31 * Handles integer difference logic (IDL) constraints. 32 */ 33 class TheoryIdl : public Theory { 34 35 /** The current model */ 36 IDLModel d_model; 37 38 /** The asserted constraints, organized by variable */ 39 IDLAssertionDB d_assertionsDB; 40 41 /** Process a new assertion, returns false if in conflict */ 42 bool processAssertion(const IDLAssertion& assertion); 43 44 public: 45 46 /** Theory constructor. */ 47 TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out, 48 Valuation valuation, const LogicInfo& logicInfo); 49 50 /** Pre-processing of input atoms */ 51 Node ppRewrite(TNode atom) override; 52 53 /** Check the assertions for satisfiability */ 54 void check(Effort effort) override; 55 56 /** Identity string */ identify()57 std::string identify() const override { return "THEORY_IDL"; } 58 59 };/* class TheoryIdl */ 60 61 }/* CVC4::theory::idl namespace */ 62 }/* CVC4::theory namespace */ 63 }/* CVC4 namespace */ 64