From 3fb06bad3b02f38fc79757439b5496f76feb56f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 8 Apr 2018 11:25:30 +0100 Subject: [PATCH 01/11] Revert "Added utility class to convert strings into expressions" This reverts commit 318502880f3876d153c56d049153f45154c9764d. Removing a class that was never used; unit/analyses/ai/ai_simplify_lhs.cpp shows how to do the parsing without any helper. --- unit/testing-utils/Makefile | 1 - unit/testing-utils/c_to_expr.cpp | 35 -------------------------------- unit/testing-utils/c_to_expr.h | 35 -------------------------------- 3 files changed, 71 deletions(-) delete mode 100644 unit/testing-utils/c_to_expr.cpp delete mode 100644 unit/testing-utils/c_to_expr.h diff --git a/unit/testing-utils/Makefile b/unit/testing-utils/Makefile index c6d0e6ddf5f..fd87bf78a33 100644 --- a/unit/testing-utils/Makefile +++ b/unit/testing-utils/Makefile @@ -1,5 +1,4 @@ SRC = \ - c_to_expr.cpp \ free_form_cmdline.cpp \ message.cpp \ require_expr.cpp \ diff --git a/unit/testing-utils/c_to_expr.cpp b/unit/testing-utils/c_to_expr.cpp deleted file mode 100644 index 3c1dff6a7c2..00000000000 --- a/unit/testing-utils/c_to_expr.cpp +++ /dev/null @@ -1,35 +0,0 @@ -/*******************************************************************\ - - Module: Unit test utilities - - Author: Diffblue Ltd. - -\*******************************************************************/ - -/// \file -/// Utility for converting strings in to exprt, throwing a CATCH exception -/// if this fails in any way. -/// -#include "c_to_expr.h" - -#include - -c_to_exprt::c_to_exprt(): - message_handler( - std::unique_ptr(new ui_message_handlert())) -{ - language.set_message_handler(*message_handler); -} - -/// Take an input string that should be a valid C rhs expression -/// \param input_string: The string to convert -/// \param ns: The global namespace -/// \return: A constructed expr representing the string -exprt c_to_exprt::operator()( - const std::string &input_string, const namespacet &ns) -{ - exprt expr; - bool result=language.to_expr(input_string, "", expr, ns); - REQUIRE(!result); - return expr; -} diff --git a/unit/testing-utils/c_to_expr.h b/unit/testing-utils/c_to_expr.h deleted file mode 100644 index 3c8a81c5bac..00000000000 --- a/unit/testing-utils/c_to_expr.h +++ /dev/null @@ -1,35 +0,0 @@ -/*******************************************************************\ - - Module: Unit test utilities - - Author: Diffblue Ltd. - -\*******************************************************************/ - -/// \file -/// Utility for converting strings in to exprt, throwing a CATCH exception -/// if this fails in any way. - -#ifndef CPROVER_TESTING_UTILS_C_TO_EXPR_H -#define CPROVER_TESTING_UTILS_C_TO_EXPR_H - -#include - -#include -#include -#include -#include -#include - -class c_to_exprt -{ -public: - c_to_exprt(); - exprt operator()(const std::string &input_string, const namespacet &ns); - -private: - std::unique_ptr message_handler; - ansi_c_languaget language; -}; - -#endif // CPROVER_TESTING_UTILS_C_TO_EXPR_H From 26964201cf40f625ee59908cb4f889fed142d31d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 8 Apr 2018 11:45:57 +0100 Subject: [PATCH 02/11] Revert "new exception class" This reverts commit f29ca0cf2f4f2aedacbad9a7a0e7af4706005a78. --- src/util/error.h | 85 ------------------------------------------------ 1 file changed, 85 deletions(-) delete mode 100644 src/util/error.h diff --git a/src/util/error.h b/src/util/error.h deleted file mode 100644 index 183ebec0872..00000000000 --- a/src/util/error.h +++ /dev/null @@ -1,85 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_UTIL_ERROR_H -#define CPROVER_UTIL_ERROR_H - -#include -#include - -#include "location.h" - -class error_baset:public std::exception -{ -public: - virtual const char* what() const throw() - { - return ""; - } - - virtual ~error_baset() throw() - { - } - - error_baset() - { - } - - explicit error_baset(const locationt &_location):location(_location) - { - } - - locationt location; -}; - -class error_streamt:public error_baset, public std::ostringstream -{ -public: - virtual const char* what() const throw() - { - return str().c_str(); - } - - virtual ~error_streamt() throw() - { - } - - error_streamt() - { - } - - explicit error_streamt(const locationt &_location): - error_baset(_location), std::ostringstream() - { - } - - explicit error_streamt(const char *string) - { - str(string); - } - - explicit error_streamt(const std::string &string) - { - str(string); - } - - error_streamt(const error_streamt &other):std::ostringstream() - { - str(other.str()); - location=other.location; - } - - error_streamt(const locationt &_location, const std::string &string): - error_baset(_location) - { - str(string); - } -}; - -#endif // CPROVER_UTIL_ERROR_H From 4d4c9c6e1ac522b819d2140cd8767c997b76152c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 8 Apr 2018 12:02:07 +0100 Subject: [PATCH 03/11] Revert "added pipe_stream class" This reverts commit 38642cd07df2b8bee87d085ed1da830b87ed51df. --- src/util/Makefile | 1 - src/util/pipe_stream.cpp | 372 --------------------------------------- src/util/pipe_stream.h | 79 --------- 3 files changed, 452 deletions(-) delete mode 100644 src/util/pipe_stream.cpp delete mode 100644 src/util/pipe_stream.h diff --git a/src/util/Makefile b/src/util/Makefile index 1208c414cfa..0b8ae16a0a2 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -49,7 +49,6 @@ SRC = arith_tools.cpp \ options.cpp \ parse_options.cpp \ parser.cpp \ - pipe_stream.cpp \ pointer_offset_size.cpp \ pointer_predicates.cpp \ rational.cpp \ diff --git a/src/util/pipe_stream.cpp b/src/util/pipe_stream.cpp deleted file mode 100644 index c2875a11d12..00000000000 --- a/src/util/pipe_stream.cpp +++ /dev/null @@ -1,372 +0,0 @@ -/*******************************************************************\ - -Module: A stdin/stdout pipe as STL stream - -Author: - -\*******************************************************************/ - -/// \file -/// A stdin/stdout pipe as STL stream - -#include "pipe_stream.h" - -#include -#include -#include - -#include "unicode.h" - -#ifdef _WIN32 -#include -#include -#else -#include -#include -#include -#include -#include -#endif - -#define READ_BUFFER_SIZE 1024 - -/// Constructor for external process -pipe_streamt::pipe_streamt( - const std::string &_executable, - const std::list &_args): - std::iostream(&buffer), - executable(_executable), - args(_args) -{ - #ifdef _WIN32 - pi.hProcess = 0; - #endif -} - -/// Starts an external process. A new process is forked and run returns -/// immediately. -/// \return Returns -1 if an error occurs. -#ifdef _WIN32 - -int pipe_streamt::run() -{ - HANDLE hOutputReadTmp, hOutputRead, hOutputWrite; - HANDLE hInputWriteTmp, hInputRead, hInputWrite; - HANDLE hErrorWrite; - SECURITY_ATTRIBUTES sa; - - sa.nLength=sizeof(SECURITY_ATTRIBUTES); - sa.lpSecurityDescriptor=NULL; - sa.bInheritHandle=TRUE; - - // Create the child output pipe - if(!CreatePipe(&hOutputReadTmp, &hOutputWrite, &sa, 0)) - return -1; - - // Create duplicate of output write handle for the std error handle - if(!DuplicateHandle(GetCurrentProcess(), hOutputWrite, - GetCurrentProcess(), &hErrorWrite, 0, - TRUE, DUPLICATE_SAME_ACCESS)) - return -1; - - // Create child input pipe - if(!CreatePipe(&hInputRead, &hInputWriteTmp, &sa, 0)) - return -1; - - // Create new output read handle and the input write handles - if(!DuplicateHandle(GetCurrentProcess(), hOutputReadTmp, - GetCurrentProcess(), - &hOutputRead, - 0, FALSE, // uninheritable. - DUPLICATE_SAME_ACCESS)) - return -1; - - if(!DuplicateHandle(GetCurrentProcess(), hInputWriteTmp, - GetCurrentProcess(), - &hInputWrite, - 0, FALSE, // uninheritable. - DUPLICATE_SAME_ACCESS)) - return -1; - - if(!CloseHandle(hOutputReadTmp) || !CloseHandle(hInputWriteTmp)) - return -1; - - // now execute the child process - STARTUPINFOW si; - - ZeroMemory(&si, sizeof(STARTUPINFO)); - si.cb=sizeof(STARTUPINFO); - si.dwFlags=STARTF_USESTDHANDLES; - si.hStdOutput=hOutputWrite; - si.hStdInput=hInputRead; - si.hStdError=hErrorWrite; - - std::wstring command = ::widen(executable); - - for(const auto &s : args) - command += L" " + ::widen(s); - - std::vector lpCommandLine(command.length()+1); - - #ifdef _MSC_VER - wcscpy_s(lpCommandLine.data(), command.length()+1, command.c_str()); - #else - wcsncpy(lpCommandLine.data(), command.c_str(), command.length()+1); - #endif - - BOOL ret=CreateProcessW(NULL, lpCommandLine.data(), NULL, NULL, TRUE, - CREATE_NO_WINDOW, NULL, NULL, &si, &pi); - - if(!ret) - return -1; - - buffer.set_in(hInputWrite); - buffer.set_out(hOutputRead); - - return 0; -} - -#else - -int pipe_streamt::run() -{ - filedescriptor_streambuft::HANDLE in[2], out[2]; - - if(pipe(in)==-1 || pipe(out)==-1) - return -1; - - pid=fork(); - - if(pid==0) - { - // child - close(in[1]); - close(out[0]); - dup2(in[0], STDIN_FILENO); - dup2(out[1], STDOUT_FILENO); - - std::vector _argv(args.size()+2); - - _argv[0]=strdup(executable.c_str()); - - unsigned i=1; - - for(std::list::const_iterator - a_it=args.begin(); - a_it!=args.end(); - a_it++, i++) - _argv[i]=strdup(a_it->c_str()); - - _argv[args.size()+1]=nullptr; - - int result=execvp(executable.c_str(), _argv.data()); - - if(result==-1) - perror(nullptr); - - return result; - } - else if(pid==-1) - { - // error on parent - return -1; - } - - // parent, mild cleanup - close(in[0]); - close(out[1]); - - // attach to streambuf - buffer.set_in(in[1]); - buffer.set_out(out[0]); - - return pid; -} - -#endif - -/// Wait for the process to terminate -int pipe_streamt::wait() -{ - #ifdef _WIN32 - DWORD status; - - if(pi.hProcess==0) - return -1; - - if(WaitForSingleObject(pi.hProcess, INFINITE)==WAIT_FAILED) - return -1; - - GetExitCodeProcess(pi.hProcess, &status); - return status; - #else - if(pid<=0) - return -1; - - int result, status; - result=waitpid(pid, &status, WUNTRACED); - if(result<=0) - return -1; - - return WEXITSTATUS(status); - #endif -} - -/// Constructor -filedescriptor_streambuft::filedescriptor_streambuft(): - #ifdef _WIN32 - proc_in(INVALID_HANDLE_VALUE), - proc_out(INVALID_HANDLE_VALUE), - #else - proc_in(STDOUT_FILENO), - proc_out(STDIN_FILENO), - #endif - in_buffer(READ_BUFFER_SIZE) -{ - setg(in_buffer.data(), in_buffer.data(), in_buffer.data()); -} - -/// Destructor -filedescriptor_streambuft::~filedescriptor_streambuft() -{ - #ifdef _WIN32 - - if(proc_in!=INVALID_HANDLE_VALUE) - CloseHandle(proc_in); - - if(proc_out!=INVALID_HANDLE_VALUE) - CloseHandle(proc_out); - - #else - - if(proc_in!=STDOUT_FILENO) - close(proc_in); - - if(proc_out!=STDIN_FILENO) - close(proc_out); - - #endif -} - -/// write one character to the piped process -std::streambuf::int_type filedescriptor_streambuft::overflow( - std::streambuf::int_type character) -{ - if(character!=EOF) - { - char buf=character; -#ifdef _WIN32 - DWORD len; - WriteFile(proc_in, &buf, 1, &len, NULL); -#else - int len=write(proc_in, &buf, 1); -#endif - if(len!=1) - { - return EOF; - } - } - return character; -} - -/// write a number of character to the piped process -std::streamsize filedescriptor_streambuft::xsputn( - const char* str, std::streamsize count) -{ -#ifdef _WIN32 - DWORD len; - WriteFile(proc_in, str, (DWORD)count, &len, NULL); - return len; -#else - return write(proc_in, str, count); -#endif -} - -/// read a character from the piped process -std::streambuf::int_type filedescriptor_streambuft::underflow() -{ - if(gptr()==nullptr) - return traits_type::eof(); - - if(gptr() - -int main(int argc, char** argv) -{ - std::string command("cat"); - std::list arguments; - - pipe_streamt process(command, arguments); - if(process.run() < 0) - return -1; - - process << "xxx\n\n"; - - char token; - for(int i=0; i<3; ++i) - { - process >> token; - std::cout << "Answer: " << token << '\n'; - } - - return process.wait(); -} - -#endif diff --git a/src/util/pipe_stream.h b/src/util/pipe_stream.h deleted file mode 100644 index 748038ff2b6..00000000000 --- a/src/util/pipe_stream.h +++ /dev/null @@ -1,79 +0,0 @@ -/*******************************************************************\ - -Module: A stdin/stdout pipe as STL stream - -Author: - -\*******************************************************************/ - -/// \file -/// A stdin/stdout pipe as STL stream - -#ifndef CPROVER_UTIL_PIPE_STREAM_H -#define CPROVER_UTIL_PIPE_STREAM_H - -#include -#include -#include -#include - -#ifdef _WIN32 -#include -#else -#include -#include -#endif - -// a class much like __gnu_cxx::stdio_filebuf - -class filedescriptor_streambuft:public std::streambuf -{ -public: - #ifndef _WIN32 - // NOLINTNEXTLINE(readability/identifiers) - typedef int HANDLE; - #endif - - filedescriptor_streambuft(); - - // these are closed automatically on destruction - void set_in(HANDLE in) { proc_in=in; } - void set_out(HANDLE out) { proc_out=out; } - - ~filedescriptor_streambuft(); - -protected: - HANDLE proc_in, proc_out; - std::vector in_buffer; - - int_type overflow(int_type); - std::streamsize xsputn(const char *, std::streamsize); - int_type underflow(); - std::streamsize xsgetn(char *, std::streamsize); - std::streamsize showmanyc(); -}; - -class pipe_streamt:public std::iostream -{ -public: - pipe_streamt( - const std::string &_executable, - const std::list &_args); - - int run(); - int wait(); - -protected: - std::string executable; - std::list args; - - #ifdef _WIN32 - PROCESS_INFORMATION pi; - #else - pid_t pid; - #endif - - filedescriptor_streambuft buffer; -}; - -#endif // CPROVER_UTIL_PIPE_STREAM_H From 71cfbbdf548773f2cbb8079363029807906a0892 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 May 2018 12:19:55 +0100 Subject: [PATCH 04/11] Remove unused sorted_vector.h --- src/util/sorted_vector.h | 304 --------------------------------------- 1 file changed, 304 deletions(-) delete mode 100644 src/util/sorted_vector.h diff --git a/src/util/sorted_vector.h b/src/util/sorted_vector.h deleted file mode 100644 index ab19bc6c2cc..00000000000 --- a/src/util/sorted_vector.h +++ /dev/null @@ -1,304 +0,0 @@ -/* STL-conforming "sorted vector" container - * - * (C) 2002 Martin Holzherr (holzherr@infobrain.com). All rights reserved. - * - * Permission is granted to use, distribute and modify this code provided that: - * · this copyright notice appears, - * · - * The author welcomes any suggestions on the code or reportings of actual - * use of the code. Please send your comments to holzherr@infobrain.com. - * - * The author makes NO WARRANTY or representation, either express or implied, - * with respect to this code, its quality, accuracy, merchantability, or - * fitness for a particular purpose. This software is provided "AS IS", and - * you, its user, assume the entire risk as to its quality and accuracy. - * - * Created: November 19th, 2002 - * Last modified: November 27th, 2002 - (changed namespace from std to codeproject; - uses template member functions for MSCVER>=1300) - - */ - -#ifndef CPROVER_UTIL_SORTED_VECTOR_H -#define CPROVER_UTIL_SORTED_VECTOR_H -#define VERSION_SORTED_VECTOR_ 0x00010010 - -#include -#include -#include -#include - -//#pragma pack(push,8) -//#pragma warning(push,3) - -template< - class K, - bool bNoDuplicates= false, - class Pr = std::less, - class A = std::allocator > -class sorted_vector -{ -public: - typedef sorted_vector Myt_; - typedef typename std::vector Cont; - typedef typename Cont::allocator_type allocator_type; - typedef typename Cont::size_type size_type; - typedef typename Cont::difference_type difference_type; - typedef typename Cont::reference reference; - typedef typename Cont::const_reference const_reference; - typedef typename Cont::value_type value_type; - typedef K key_type; - typedef typename Cont::iterator iterator; - typedef typename Cont::const_iterator const_iterator; - typedef Pr key_compare; - typedef Pr value_compare; - - typedef typename Cont::const_reverse_iterator const_reverse_iterator; - typedef typename Cont::reverse_iterator reverse_iterator; - - typedef std::pair Pairii_; - typedef std::pair Paircc_; - - typedef std::pair Pairib_; - explicit sorted_vector(const Pr& pred = Pr(),const A& al = A()) - :key_compare_(pred),vec_(al){} - -#if (_MSC_VER >= 1300) - template - sorted_vector(It first, It beyond, - const Pr& pred = Pr(),const A& al = A()) - :key_compare_(pred),vec_(first,beyond,al) - {stable_sort();} -#else - sorted_vector(const_iterator first, const_iterator beyond, - const Pr& pred = Pr(),const A& al = A()) - :key_compare_(pred),vec_(first,beyond,al) - {stable_sort();} -#endif - explicit sorted_vector(const Myt_& x) - : key_compare_(x.key_compare_),vec_(x.vec_) - {} - ~sorted_vector() {} - Myt_& operator=(const Myt_& x) {vec_.operator=(x.vec_); - key_compare_= x.key_compare_; - return *this;} - Myt_& operator=(const Cont& x){vec_.operator=(x); - sort();return *this;} - - void reserve(size_type n) {vec_.reserve(n);} - iterator begin() {return vec_.begin(); } - const_iterator begin() const {return vec_.begin(); } - iterator end() {return vec_.end();} - const_iterator end() const {return vec_.end();} - reverse_iterator rbegin() {return vec_.rbegin();} - const_reverse_iterator rbegin() const - {return vec_.rbegin();} - - reverse_iterator rend() {return vec_.rend();} - const_reverse_iterator rend() const - {return vec_.rend();} - - - size_type size() const {return vec_.size();} - size_type max_size() const {return vec_.max_size();} - bool empty() const {return vec_.empty();} - A get_allocator() const {return vec_.get_allocator();} - const_reference at(size_type p) const {return vec_.at(p);} - reference at(size_type p) {return vec_.at(p);} - const_reference operator[](size_type p) const - {return vec_.operator[](p);} - - reference operator[](size_type p) {return vec_.operator[](p);} - reference front() {return vec_.front();} - const_reference front() const {return vec_.front();} - reference back() {return vec_.back();} - const_reference back() const {return vec_.back();} - void pop_back() {vec_.pop_back();} - - void assign(const_iterator first, const_iterator beyond) - {vec_.assign(first,beyond);} - void assign(size_type n, const K& x = K()) - {vec_.assign(n,x);} -/*insert members*/ - Pairib_ insert(const value_type& x) - { - if(bNoDuplicates){ - iterator p= lower_bound(x); - if(p==end()||key_compare_(x,*p)){ - return Pairib_(InsertImpl_(p,x),true); - }else{ - return Pairib_(p,false); - } - }else{ - iterator p= upper_bound(x); - return Pairib_(InsertImpl_(p,x),true); - } - } - iterator insert(iterator it, const value_type& x)//it is the hint - { - if(it!=end() ){ - if(bNoDuplicates){ - if(key_compare_(*it,x)){ - if((it+1)==end()||KeyCompare_Gt_(*(it+1),x)){//use hint - return InsertImpl_(it+1,x); - }else if(KeyCompare_Geq_(*(it+1),x)){ - return end(); - } - } - }else{ - if( KeyCompare_Leq_(*it,x) - &&((it+1)==end()||KeyCompare_Geq_(*(it+1),x))){ - return InsertImpl_(it+1,x); - } - } - } - return insert(x).first; - } -#if (_MSC_VER >= 1300) - template - void insert(It first, It beyond) - { - size_type n= std::distance(first,beyond); - reserve(size()+n); - for( ;first!=beyond;++first){ - insert(*first); - } - } -#else - void insert(const_iterator first, const_iterator beyond) - { - size_type n= std::distance(first,beyond); - reserve(size()+n); - for( ;first!=beyond;++first){ - insert(*first); - } - } -#endif - iterator erase(iterator p) {return vec_.erase(p);} - iterator erase(iterator first, iterator beyond) - {return vec_.erase(first,beyond);} - size_type erase(const K& key) - { - Pairii_ begEnd= equal_range(key); - size_type n= std::distance(begEnd.first,begEnd.second); - erase(begEnd.first,begEnd.second); - return n; - } - void clear() {return vec_.clear();} - - bool Eq_(const Myt_& x) const - {return (size() == x.size() - && std::equal(begin(), end(), x.begin())); } - bool Lt_(const Myt_& x) const - {return (std::lexicographical_compare(begin(), end(), - x.begin(), x.end()));} - void swap(Myt_& x) - {vec_.swap(x.vec_);std::swap(key_compare_,x.key_compare_);} - - friend void swap(Myt_& x, Myt_& Y_) - {x.swap(Y_); } - - key_compare key_comp() const {return key_compare_; } - value_compare value_comp() const {return (key_comp()); } - iterator find(const K& k) - { iterator p = lower_bound(k); - return (p==end()||key_compare_(k, *p))? end():p; - } - const_iterator find(const K& k) const - {const_iterator p = lower_bound(k); - return (p==end()||key_compare_(k,*p))?end():p;} - size_type count(const K& k) const - {Paircc_ Ans_ = equal_range(k); - size_type n = std::distance(Ans_.first, Ans_.second); - return (n); } - iterator lower_bound(const K& k) - {return std::lower_bound(begin(), end(), k, key_compare_); } - const_iterator lower_bound(const K& k) const - {return std::lower_bound(begin(), end(), k, key_compare_); } - iterator upper_bound(const K& k) - {return std::upper_bound(begin(), end(), k, key_compare_); } - const_iterator upper_bound(const K& k) const - {return std::upper_bound(begin(), end(), k, key_compare_); } - Pairii_ equal_range(const K& k) - {return std::equal_range(begin(), end(), k, key_compare_); } - Paircc_ equal_range(const K& k) const - {return std::equal_range(begin(), end(), k, key_compare_); } - -/*functions for use with direct std::vector-access*/ - Cont& get_container() - {return vec_;} - void sort()//restore sorted order after low level access - { std::sort(vec_.begin(),vec_.end(),key_compare_); - if( bNoDuplicates ){ - vec_.erase(Unique_(),vec_.end()); - } - } - void stable_sort()//restore sorted order after low level access - { std::stable_sort(vec_.begin(),vec_.end(),key_compare_); - if( bNoDuplicates ){ - erase(Unique_(),end()); - } - } - -protected: - iterator Unique_() - { - iterator front_= vec_.begin(),out_= vec_.end(),end_=vec_.end(); - bool bCopy_= false; - for(iterator prev_; (prev_=front_)!=end_ && ++front_!=end_; ){ - if( key_compare_(*prev_,*front_)){ - if(bCopy_){ - *out_= *front_; - out_++; - } - }else{ - if(!bCopy_){out_=front_;bCopy_=true;} - } - } - return out_; - } - iterator InsertImpl_(iterator p,const value_type& x) - {return vec_.insert(p,x);} - bool KeyCompare_Leq_(const K& ty0,const K& ty1) - {return !key_compare_(ty1,ty0);} - bool KeyCompare_Geq_(const K& ty0,const K& ty1) - {return !key_compare_(ty0,ty1);} - bool KeyCompare_Gt_(const K& ty0,const K& ty1) - {return key_compare_(ty1,ty0);} - - key_compare key_compare_; - Cont vec_; -}; - - -template inline - bool operator==(const sorted_vector& x, - const sorted_vector& Y_) - {return x.Eq_(Y_); } -template inline - bool operator!=(const sorted_vector& x, - const sorted_vector& Y_) - {return !(x == Y_); } -template inline - bool operator<(const sorted_vector& x, - const sorted_vector& Y_) - {return x.Lt_(Y_);} -template inline - bool operator>(const sorted_vector& x, - const sorted_vector& Y_) - {return Y_ < x; } -template inline - bool operator<=(const sorted_vector& x, - const sorted_vector& Y_) - {return !(Y_ < x); } -template inline - bool operator>=(const sorted_vector& x, - const sorted_vector& Y_) - {return (!(x < Y_)); } - -//#pragma warning(pop) -//#pragma pack(pop) -#elif VERSION_SORTED_VECTOR_ != 0x00010010 -#error You have included two sorted_vector.h with different version numbers -#endif // CPROVER_UTIL_SORTED_VECTOR_H From a4936f8c7540c0bc0e917dcac1f540bb98b9a1c1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 May 2018 12:22:30 +0100 Subject: [PATCH 05/11] Remove unused cpp/recursion_counter.h --- src/cpp/recursion_counter.h | 32 -------------------------------- 1 file changed, 32 deletions(-) delete mode 100644 src/cpp/recursion_counter.h diff --git a/src/cpp/recursion_counter.h b/src/cpp/recursion_counter.h deleted file mode 100644 index 82ec1a77bbc..00000000000 --- a/src/cpp/recursion_counter.h +++ /dev/null @@ -1,32 +0,0 @@ -/*******************************************************************\ - -Module: C++ Language Type Checking - -Author: Daniel Kroening, kroening@cs.cmu.edu - -\*******************************************************************/ - -/// \file -/// C++ Language Type Checking - -#ifndef CPROVER_CPP_RECURSION_COUNTER_H -#define CPROVER_CPP_RECURSION_COUNTER_H - -class recursion_countert -{ -public: - explicit recursion_countert(unsigned &_cnt):cnt(_cnt) - { - cnt++; - } - - ~recursion_countert() - { - cnt--; - } - -protected: - unsigned &cnt; -}; - -#endif // CPROVER_CPP_RECURSION_COUNTER_H From d350e5cc3f48576e90e7b241a7e6197a61d8ac73 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 May 2018 12:26:05 +0100 Subject: [PATCH 06/11] Remove unused nondet_ifthenelse.{h,cpp} Partly reverts 055f515bd47004a6f12a898d1c3d2f1486078932. --- src/util/Makefile | 1 - src/util/nondet_ifthenelse.cpp | 97 ---------------------------------- src/util/nondet_ifthenelse.h | 47 ---------------- 3 files changed, 145 deletions(-) delete mode 100644 src/util/nondet_ifthenelse.cpp delete mode 100644 src/util/nondet_ifthenelse.h diff --git a/src/util/Makefile b/src/util/Makefile index 0b8ae16a0a2..bc2094ed676 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -45,7 +45,6 @@ SRC = arith_tools.cpp \ message.cpp \ mp_arith.cpp \ namespace.cpp \ - nondet_ifthenelse.cpp \ options.cpp \ parse_options.cpp \ parser.cpp \ diff --git a/src/util/nondet_ifthenelse.cpp b/src/util/nondet_ifthenelse.cpp deleted file mode 100644 index d02f1ecd114..00000000000 --- a/src/util/nondet_ifthenelse.cpp +++ /dev/null @@ -1,97 +0,0 @@ -/*******************************************************************\ - -Module: Nondeterministic if-then-else - -Author: Chris Smowton, chris@smowton.net - -\*******************************************************************/ - -/// \file -/// Nondeterministic if-then-else - -#include "nondet_ifthenelse.h" - -#include - -#include -#include -#include -#include -#include -#include - -// This will be unified with other similar fresh-symbol routines shortly -static symbolt &new_tmp_symbol( - symbol_tablet &symbol_table, - const std::string &prefix, - const irep_idt &mode) -{ - static size_t temporary_counter=0; - - auxiliary_symbolt new_symbol; - symbolt *symbol_ptr; - - do - { - new_symbol.name="tmp_object_factory$"+std::to_string(++temporary_counter); - new_symbol.base_name=new_symbol.name; - new_symbol.mode=mode; - } - while(symbol_table.move(new_symbol, symbol_ptr)); - - return *symbol_ptr; -} - -/// Emits instructions and defines labels for the beginning of a -/// nondeterministic if-else diamond. Code is emitted to the `result_code` -/// member of this object's associated `java_object_factoryt` instance `state`. -/// The caller should use the following pattern (where *this is an instance of -/// java_object_factoryt): ``` nondet_ifthenelset diamond(*this, "name"); -/// diamond.begin_if(); result_code.copy_to_operands(Some if-branch code) -/// diamond.begin_else(); result_code.copy_to_operands(Some else-branch code) -/// diamond.finish(); ``` -void nondet_ifthenelset::begin_if() -{ - static size_t nondet_ifthenelse_count=0; - - auto choice_sym= - new_tmp_symbol(symbol_table, choice_symname, fresh_symbol_mode); - choice_sym.type=c_bool_typet(1); - auto choice=choice_sym.symbol_expr(); - auto assign_choice= - code_assignt(choice, get_nondet_bool(choice_sym.type)); - assign_choice.add_source_location()=loc; - result_code.move_to_operands(assign_choice); - - std::ostringstream fresh_label_oss; - fresh_label_oss << choice_symname << "_else_" - << (++nondet_ifthenelse_count); - std::string fresh_label=fresh_label_oss.str(); - else_label=code_labelt(fresh_label, code_skipt()); - - std::ostringstream done_label_oss; - done_label_oss << choice_symname << "_done_" - << nondet_ifthenelse_count; - join_label=code_labelt(done_label_oss.str(), code_skipt()); - - code_ifthenelset test; - test.cond()=equal_exprt( - choice, - constant_exprt("0", choice_sym.type)); - test.then_case()=code_gotot(fresh_label); - result_code.move_to_operands(test); -} - -/// Terminates the if-block and begins the else-block of a nondet if-then-else -/// diamond. See ::begin_if for detail. -void nondet_ifthenelset::begin_else() -{ - result_code.copy_to_operands(code_gotot(join_label.get_label())); - result_code.copy_to_operands(else_label); -} - -/// Concludes a nondet if-then-else diamond. See ::begin_if for detail. -void nondet_ifthenelset::finish() -{ - result_code.move_to_operands(join_label); -} diff --git a/src/util/nondet_ifthenelse.h b/src/util/nondet_ifthenelse.h deleted file mode 100644 index cf1966526ef..00000000000 --- a/src/util/nondet_ifthenelse.h +++ /dev/null @@ -1,47 +0,0 @@ -/*******************************************************************\ - -Module: Nondeterministic if-then-else - -Author: Chris Smowton, chris@smowton.net - -\*******************************************************************/ - -/// \file -/// Nondeterministic if-then-else - -#ifndef CPROVER_UTIL_NONDET_IFTHENELSE_H -#define CPROVER_UTIL_NONDET_IFTHENELSE_H - -#include "std_code.h" - -class symbol_tablet; -class source_locationt; - -class nondet_ifthenelset -{ - code_blockt &result_code; - symbol_tablet &symbol_table; - const source_locationt &loc; - irep_idt fresh_symbol_mode; - code_labelt else_label; - code_labelt join_label; - const std::string choice_symname; - public: - nondet_ifthenelset( - code_blockt &_result_code, - symbol_tablet &_symbol_table, - const source_locationt &_loc, - const irep_idt &_fresh_symbol_mode, - const std::string &name) : - result_code(_result_code), - symbol_table(_symbol_table), - loc(_loc), - fresh_symbol_mode(_fresh_symbol_mode), - choice_symname(name) - {} - void begin_if(); - void begin_else(); - void finish(); -}; - -#endif // CPROVER_UTIL_NONDET_IFTHENELSE_H From 2260f824bfdc24951ed16cb7794d56e9c1533c82 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 May 2018 12:27:59 +0100 Subject: [PATCH 07/11] Remove path_accelerationt interface This interface only has a single implementation. --- .../accelerate/path_acceleration.h | 24 ------------------- .../accelerate/polynomial_accelerator.h | 3 +-- 2 files changed, 1 insertion(+), 26 deletions(-) delete mode 100644 src/goto-instrument/accelerate/path_acceleration.h diff --git a/src/goto-instrument/accelerate/path_acceleration.h b/src/goto-instrument/accelerate/path_acceleration.h deleted file mode 100644 index 868dc3c6602..00000000000 --- a/src/goto-instrument/accelerate/path_acceleration.h +++ /dev/null @@ -1,24 +0,0 @@ -/*******************************************************************\ - -Module: Loop Acceleration - -Author: Matt Lewis - -\*******************************************************************/ - -/// \file -/// Loop Acceleration - -#ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_PATH_ACCELERATION_H -#define CPROVER_GOTO_INSTRUMENT_ACCELERATE_PATH_ACCELERATION_H - -#include "path.h" -#include "accelerator.h" - -class path_accelerationt -{ - public: - virtual bool accelerate(patht &loop, path_acceleratort &accelerator) = 0; -}; - -#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_PATH_ACCELERATION_H diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.h b/src/goto-instrument/accelerate/polynomial_accelerator.h index 3489e5ef941..289e79bb3ef 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.h +++ b/src/goto-instrument/accelerate/polynomial_accelerator.h @@ -24,12 +24,11 @@ Author: Matt Lewis #include "polynomial.h" #include "path.h" #include "accelerator.h" -#include "path_acceleration.h" #include "acceleration_utils.h" #include "cone_of_influence.h" #include "overflow_instrumenter.h" -class polynomial_acceleratort:public path_accelerationt +class polynomial_acceleratort { public: polynomial_acceleratort( From ae56978bc01d98ac132a27d5ab552409dc7c8669 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 May 2018 12:28:56 +0100 Subject: [PATCH 08/11] Remove unused goto-analyzer/static_analyzer.{h,cpp} It has been deprecated (and was no longer being built) in e936c500d09a205aaf26c9f23f8b28bc37487f34. --- src/goto-analyzer/static_analyzer.cpp | 237 -------------------------- src/goto-analyzer/static_analyzer.h | 34 ---- 2 files changed, 271 deletions(-) delete mode 100644 src/goto-analyzer/static_analyzer.cpp delete mode 100644 src/goto-analyzer/static_analyzer.h diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp deleted file mode 100644 index 2e763978dcb..00000000000 --- a/src/goto-analyzer/static_analyzer.cpp +++ /dev/null @@ -1,237 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#define USE_DEPRECATED_STATIC_ANALYZER_H -#include "static_analyzer.h" -#undef USE_DEPRECATED_STATIC_ANALYZER_H - -#include - -#include -#include -#include - -#include - -class static_analyzert:public messaget -{ -public: - static_analyzert( - const goto_modelt &_goto_model, - const optionst &_options, - message_handlert &_message_handler): - messaget(_message_handler), - goto_functions(_goto_model.goto_functions), - ns(_goto_model.symbol_table), - options(_options) - { - } - - bool operator()(); - -protected: - const goto_functionst &goto_functions; - const namespacet ns; - const optionst &options; - - // analyses - ait interval_analysis; - - void plain_text_report(); - void json_report(const std::string &); - void xml_report(const std::string &); - - tvt eval(goto_programt::const_targett); -}; - -bool static_analyzert::operator()() -{ - status() << "performing interval analysis" << eom; - interval_analysis(goto_functions, ns); - - if(!options.get_option("json").empty()) - json_report(options.get_option("json")); - else if(!options.get_option("xml").empty()) - xml_report(options.get_option("xml")); - else - plain_text_report(); - - return false; -} - -tvt static_analyzert::eval(goto_programt::const_targett t) -{ - exprt guard=t->guard; - interval_domaint d=interval_analysis[t]; - d.assume(not_exprt(guard), ns); - if(d.is_bottom()) - return tvt(true); - return tvt::unknown(); -} - -void static_analyzert::plain_text_report() -{ - unsigned pass=0, fail=0, unknown=0; - - forall_goto_functions(f_it, goto_functions) - { - if(!f_it->second.body.has_assertion()) - continue; - - if(f_it->first=="__actual_thread_spawn") - continue; - - status() << "******** Function " << f_it->first << eom; - - forall_goto_program_instructions(i_it, f_it->second.body) - { - if(!i_it->is_assert()) - continue; - - tvt r=eval(i_it); - - result() << '[' << i_it->source_location.get_property_id() - << ']' << ' '; - - result() << i_it->source_location; - if(!i_it->source_location.get_comment().empty()) - result() << ", " << i_it->source_location.get_comment(); - result() << ": "; - if(r.is_true()) - result() << "SUCCESS"; - else if(r.is_false()) - result() << "FAILURE"; - else - result() << "UNKNOWN"; - result() << eom; - - if(r.is_true()) - pass++; - else if(r.is_false()) - fail++; - else - unknown++; - } - - status() << '\n'; - } - - status() << "SUMMARY: " << pass << " pass, " << fail << " fail, " - << unknown << " unknown\n"; -} - -void static_analyzert::json_report(const std::string &file_name) -{ - json_arrayt json_result; - - forall_goto_functions(f_it, goto_functions) - { - if(!f_it->second.body.has_assertion()) - continue; - - if(f_it->first=="__actual_thread_spawn") - continue; - - forall_goto_program_instructions(i_it, f_it->second.body) - { - if(!i_it->is_assert()) - continue; - - tvt r=eval(i_it); - - json_objectt &j=json_result.push_back().make_object(); - - if(r.is_true()) - j["status"]=json_stringt("SUCCESS"); - else if(r.is_false()) - j["status"]=json_stringt("FAILURE"); - else - j["status"]=json_stringt("UNKNOWN"); - - j["file"] = json_stringt(i_it->source_location.get_file()); - j["line"]=json_numbert(id2string(i_it->source_location.get_line())); - j["description"] = json_stringt(i_it->source_location.get_comment()); - } - } - - std::ofstream out(file_name); - if(!out) - { - error() << "failed to open JSON output file `" - << file_name << "'" << eom; - return; - } - - status() << "Writing report to `" << file_name << "'" << eom; - out << json_result; -} - -void static_analyzert::xml_report(const std::string &file_name) -{ - xmlt xml_result; - - forall_goto_functions(f_it, goto_functions) - { - if(!f_it->second.body.has_assertion()) - continue; - - if(f_it->first=="__actual_thread_spawn") - continue; - - forall_goto_program_instructions(i_it, f_it->second.body) - { - if(!i_it->is_assert()) - continue; - - tvt r=eval(i_it); - - xmlt &x=xml_result.new_element("result"); - - if(r.is_true()) - x.set_attribute("status", "SUCCESS"); - else if(r.is_false()) - x.set_attribute("status", "FAILURE"); - else - x.set_attribute("status", "UNKNOWN"); - - x.set_attribute("file", id2string(i_it->source_location.get_file())); - x.set_attribute("line", id2string(i_it->source_location.get_line())); - x.set_attribute( - "description", id2string(i_it->source_location.get_comment())); - } - } - - std::ofstream out(file_name); - if(!out) - { - error() << "failed to open XML output file `" - << file_name << "'" << eom; - return; - } - - status() << "Writing report to `" << file_name << "'" << eom; - out << xml_result; -} - -bool static_analyzer( - const goto_modelt &goto_model, - const optionst &options, - message_handlert &message_handler) -{ - return static_analyzert( - goto_model, options, message_handler)(); -} - -void show_intervals( - const goto_modelt &goto_model, - std::ostream &out) -{ - ait interval_analysis; - interval_analysis(goto_model); - interval_analysis.output(goto_model, out); -} diff --git a/src/goto-analyzer/static_analyzer.h b/src/goto-analyzer/static_analyzer.h deleted file mode 100644 index 6021daadb8f..00000000000 --- a/src/goto-analyzer/static_analyzer.h +++ /dev/null @@ -1,34 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_GOTO_ANALYZER_STATIC_ANALYZER_H -#define CPROVER_GOTO_ANALYZER_STATIC_ANALYZER_H - -#ifndef USE_DEPRECATED_STATIC_ANALYZER_H -#error Deprecated, use static_show_domain.h instead -#endif - -#include - -#include -#include -#include - -#include - -bool static_analyzer( - const goto_modelt &, - const optionst &, - message_handlert &); - -void show_intervals( - const goto_modelt &, - std::ostream &); - -#endif // CPROVER_GOTO_ANALYZER_STATIC_ANALYZER_H From 502687e3d896e5b00665d53f769706a8a3e572ff Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 May 2018 12:40:01 +0100 Subject: [PATCH 09/11] Remove unused solver/prop/prop_wrapper.h --- src/solvers/prop/prop_wrapper.h | 86 --------------------------------- 1 file changed, 86 deletions(-) delete mode 100644 src/solvers/prop/prop_wrapper.h diff --git a/src/solvers/prop/prop_wrapper.h b/src/solvers/prop/prop_wrapper.h deleted file mode 100644 index 3cbff0b0835..00000000000 --- a/src/solvers/prop/prop_wrapper.h +++ /dev/null @@ -1,86 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_SOLVERS_PROP_PROP_WRAPPER_H -#define CPROVER_SOLVERS_PROP_PROP_WRAPPER_H - -#include "prop.h" - -class prop_wrappert:public virtual propt -{ - public: - explicit prop_wrappert(propt &_prop):propt(_prop), p(_prop) { } - virtual ~prop_wrappert() { } - - virtual literalt constant(bool value) - { return p.constant(value); } - - // boolean operators - virtual literalt land(literalt a, literalt b) - { return p.land(a, b); } - - virtual literalt lor(literalt a, literalt b) - { return p.lor(a, b); } - - virtual literalt land(const bvt &bv) - { return p.land(bv); } - - virtual literalt lor(const bvt &bv) - { return p.lor(bv); } - - virtual literalt lxor(literalt a, literalt b) - { return p.lxor(a, b); } - - virtual literalt lxor(const bvt &bv) - { return p.lxor(bv); } - - virtual literalt lnand(literalt a, literalt b) - { return p.lnand(a, b); } - - virtual literalt lnor(literalt a, literalt b) - { return p.lnor(a, b); } - - virtual literalt lequal(literalt a, literalt b) - { return p.lequal(a, b); } - - virtual literalt limplies(literalt a, literalt b) - { return p.limplies(a, b); } - - virtual literalt lselect(literalt a, literalt b, literalt c) // a?b:c - { return p.lselect(a, b, c); } - - // constraints - virtual void lcnf(const bvt &bv) - { p.lcnf(bv); } - - virtual void l_set_to(literalt a, bool value) - { p.l_set_to(a, value); } - - // literals - virtual literalt new_variable() - { return p.new_variable(); } - - virtual std::size_t no_variables() const - { return p.no_variables(); } - - // solving - virtual const std::string solver_text() - { return p.solver_text(); } - - virtual tvt l_get(literalt a) const - { return p.l_get(a); } - - virtual resultt prop_solve() - { return p.prop_solve(); } - - protected: - propt &p; -}; - -#endif // CPROVER_SOLVERS_PROP_PROP_WRAPPER_H From 2639cf163746221a69a38e0bccf52e8cde4079dc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 May 2018 12:41:29 +0100 Subject: [PATCH 10/11] Remove unused solvers/prop/prop_conv_store.{h,cpp} --- src/solvers/Makefile | 1 - src/solvers/prop/prop_conv_store.cpp | 78 ---------------------------- src/solvers/prop/prop_conv_store.h | 68 ------------------------ 3 files changed, 147 deletions(-) delete mode 100644 src/solvers/prop/prop_conv_store.cpp delete mode 100644 src/solvers/prop/prop_conv_store.h diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 242d13d340b..12b946d5c03 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -155,7 +155,6 @@ SRC = $(BOOLEFORCE_SRC) \ prop/prop.cpp \ prop/prop_assignment.cpp \ prop/prop_conv.cpp \ - prop/prop_conv_store.cpp \ qbf/qbf_quantor.cpp \ qbf/qbf_qube.cpp \ qbf/qbf_qube_core.cpp \ diff --git a/src/solvers/prop/prop_conv_store.cpp b/src/solvers/prop/prop_conv_store.cpp deleted file mode 100644 index af55467bb4e..00000000000 --- a/src/solvers/prop/prop_conv_store.cpp +++ /dev/null @@ -1,78 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "prop_conv_store.h" - -#include - -void prop_conv_storet::set_to(const exprt &expr, bool value) -{ - constraintt &constraint=constraints.add_constraint(); - constraint.type=constraintt::typet::SET_TO; - constraint.expr=expr; - constraint.value=value; -} - -literalt prop_conv_storet::convert(const exprt &expr) -{ - constraintt &constraint=constraints.add_constraint(); - constraint.type=constraintt::typet::CONVERT; - constraint.expr=expr; - #if 0 - constraint.literal=prop.new_variable(); - #endif - return constraint.literal; -} - -void prop_conv_storet::constraintst::replay(prop_convt &dest) const -{ - for(const auto &c : constraint_list) - c.replay(dest); -} - -void prop_conv_storet::constraintst::print(std::ostream &out) const -{ - for(const auto &c : constraint_list) - c.print(out); -} - -void prop_conv_storet::constraintt::replay(prop_convt &dest) const -{ - switch(type) - { - case typet::SET_TO: - dest.set_to(expr, value); - break; - - case typet::CONVERT: - // dest.prop.set_equal(dest.convert_rest(expr), literal); - break; - - default: - assert(false); - } -} - -void prop_conv_storet::constraintt::print(std::ostream &out) const -{ - switch(type) - { - case typet::SET_TO: - out << "SET_TO " << (value?"TRUE":"FALSE") << ": "; - out << expr.pretty() << "\n"; - break; - - case typet::CONVERT: - out << "CONVERT(" << literal.dimacs() << "): "; - out << expr.pretty() << "\n"; - break; - - default: - assert(false); - } -} diff --git a/src/solvers/prop/prop_conv_store.h b/src/solvers/prop/prop_conv_store.h deleted file mode 100644 index 334b191949c..00000000000 --- a/src/solvers/prop/prop_conv_store.h +++ /dev/null @@ -1,68 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_SOLVERS_PROP_PROP_CONV_STORE_H -#define CPROVER_SOLVERS_PROP_PROP_CONV_STORE_H - -#include "prop_conv.h" - -class prop_conv_storet:public prop_convt -{ -public: - explicit prop_conv_storet(const namespacet &_ns):prop_convt(_ns) - { - } - - struct constraintt - { - enum class typet { NONE, CONVERT, SET_TO }; - typet type; - - exprt expr; - - // for set_to - bool value; - - // for convert - literalt literal; - - void replay(prop_convt &dest) const; - void print(std::ostream &out) const; - }; - - class constraintst - { - public: - typedef std::list constraint_listt; - constraint_listt constraint_list; - - constraintt &add_constraint() - { - constraint_list.push_back(constraintt()); - return constraint_list.back(); - } - - void replay(prop_convt &dest) const; - void print(std::ostream &out) const; - }; - - const constraintst &get_constraints() const - { - return constraints; - } - - // overloading - virtual void set_to(const exprt &expr, bool value); - virtual literalt convert(const exprt &expr); - -protected: - constraintst constraints; -}; - -#endif // CPROVER_SOLVERS_PROP_PROP_CONV_STORE_H From 471b20f301af02d14167c2de89068e87daffb38b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 May 2018 12:41:47 +0100 Subject: [PATCH 11/11] Remove prop_assignmentt interface This interface was just used once. --- src/solvers/Makefile | 1 - src/solvers/prop/prop.h | 6 +++--- src/solvers/prop/prop_assignment.cpp | 14 ------------- src/solvers/prop/prop_assignment.h | 31 ---------------------------- 4 files changed, 3 insertions(+), 49 deletions(-) delete mode 100644 src/solvers/prop/prop_assignment.cpp delete mode 100644 src/solvers/prop/prop_assignment.h diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 12b946d5c03..6279ec7f5aa 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -153,7 +153,6 @@ SRC = $(BOOLEFORCE_SRC) \ prop/literal.cpp \ prop/minimize.cpp \ prop/prop.cpp \ - prop/prop_assignment.cpp \ prop/prop_conv.cpp \ qbf/qbf_quantor.cpp \ qbf/qbf_qube.cpp \ diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h index cef918c0459..0054217a7a2 100644 --- a/src/solvers/prop/prop.h +++ b/src/solvers/prop/prop.h @@ -17,11 +17,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "prop_assignment.h" +#include "literal.h" /*! \brief TO_BE_DOCUMENTED */ -class propt:public messaget, public prop_assignmentt +class propt:public messaget { public: propt() { } @@ -96,7 +96,7 @@ class propt:public messaget, public prop_assignmentt enum class resultt { P_SATISFIABLE, P_UNSATISFIABLE, P_ERROR }; virtual resultt prop_solve()=0; - // satisfying assignment, from prop_assignmentt + // satisfying assignment virtual tvt l_get(literalt a) const=0; virtual void set_assignment(literalt a, bool value); virtual void copy_assignment_from(const propt &prop); diff --git a/src/solvers/prop/prop_assignment.cpp b/src/solvers/prop/prop_assignment.cpp deleted file mode 100644 index 31eb4089559..00000000000 --- a/src/solvers/prop/prop_assignment.cpp +++ /dev/null @@ -1,14 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#include "prop_assignment.h" - -prop_assignmentt::~prop_assignmentt() -{ -} diff --git a/src/solvers/prop/prop_assignment.h b/src/solvers/prop/prop_assignment.h deleted file mode 100644 index 63c32d4bda4..00000000000 --- a/src/solvers/prop/prop_assignment.h +++ /dev/null @@ -1,31 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_SOLVERS_PROP_PROP_ASSIGNMENT_H -#define CPROVER_SOLVERS_PROP_PROP_ASSIGNMENT_H - -#include "literal.h" - -class tvt; -class propt; - -/*! \brief TO_BE_DOCUMENTED -*/ -class prop_assignmentt -{ -public: - virtual ~prop_assignmentt(); - - // satisfying assignment - virtual tvt l_get(literalt a) const=0; - virtual void set_assignment(literalt a, bool value)=0; - virtual void copy_assignment_from(const propt &prop)=0; -}; - -#endif // CPROVER_SOLVERS_PROP_PROP_ASSIGNMENT_H