diff --git a/Application.cpp b/Application.cpp index 1980ab0..7950c63 100644 --- a/Application.cpp +++ b/Application.cpp @@ -23,8 +23,13 @@ Application::Application(int &argc, char** argv[]) this->m_appSettings = new QSettings(); this->checkSettings(); - connect(this, &Application::signal_triggerQuantor, + // Application -> Quantor + connect(this, &Application::signal_quantorTriggered, &m_quantorInterface, &quantor::QuantorInterface::slot_solveProblem); + + // Quantor -> Application + connect(&m_quantorInterface, &quantor::QuantorInterface::signal_hasSolution, + this, &Application::signal_quantorSolutionAvailable); } Application::~Application() { diff --git a/Application.h b/Application.h index 2632366..743b21b 100644 --- a/Application.h +++ b/Application.h @@ -30,7 +30,13 @@ class Application : public QApplication { static Application* instance(); signals: - void signal_triggerQuantor(Document* document, QString targetFunction); + + // --- forwarded signals --- + // ApplicationContext -> Quantor + void signal_quantorTriggered(Document* document, QString targetFunction); + + // Quantor -> ApplicationContext -> MainWindow + void signal_quantorSolutionAvailable(QString, const QMap*); public slots: void slot_resetSettings(); diff --git a/ApplicationContext.cpp b/ApplicationContext.cpp index cf7ee0a..2294409 100644 --- a/ApplicationContext.cpp +++ b/ApplicationContext.cpp @@ -76,6 +76,8 @@ ApplicationContext::setupSignalsAndSlots() { connect(this, &ApplicationContext::signal_showDocument, m_mainWindow, static_cast (&MainWindow::slot_openDocumentTab)); // ship around overloaded function + connect(this, &ApplicationContext::signal_quantorSolutionAvailable, + m_mainWindow, &MainWindow::slot_displayQuantorResult); // saving signal has to be set up by project // ApplicationContext -> ComponentFactory @@ -90,7 +92,11 @@ ApplicationContext::setupSignalsAndSlots() { // ApplicationContext -> Application connect(this, &ApplicationContext::signal_triggerQuantor, - m_application, &Application::signal_triggerQuantor); + m_application, &Application::signal_quantorTriggered); + + // Application -> ApplicationContext + connect(m_application, &Application::signal_quantorSolutionAvailable, + this, &ApplicationContext::signal_quantorSolutionAvailable); } diff --git a/ApplicationContext.h b/ApplicationContext.h index f5c15c4..692d2d6 100644 --- a/ApplicationContext.h +++ b/ApplicationContext.h @@ -59,8 +59,10 @@ class ApplicationContext : public QObject { void signal_clearComponentTypes(); void signal_triggerQuantor(Document* document, QString targetFunction); + // forwarding signal to MainWindow void signal_showDocument(Document* document); + void signal_quantorSolutionAvailable(QString, const QMap*); public slots: void slot_newDocument(QString name); diff --git a/MapModel.cpp b/MapModel.cpp new file mode 100644 index 0000000..45c86fc --- /dev/null +++ b/MapModel.cpp @@ -0,0 +1,39 @@ +#include "MapModel.h" + +using namespace q2d::util; + +MapModel::MapModel(QObject *parent) : + QAbstractTableModel(parent) +{ + m_map = nullptr; +} + +int MapModel::rowCount(const QModelIndex& parent) const +{ + Q_UNUSED(parent); + if (m_map) + return m_map->count(); + return 0; +} + +int MapModel::columnCount(const QModelIndex & parent) const +{ + Q_UNUSED(parent); + return 2; +} + +QVariant MapModel::data(const QModelIndex& index, int role) const +{ + if (m_map == nullptr) + return QVariant(); + if (index.row() < 0 || + index.row() >= m_map->count() || + role != Qt::DisplayRole) { + return QVariant(); + } + if (index.column() == 0) + return m_map->keys().at(index.row()); + if (index.column() == 1) + return m_map->values().at(index.row()); + return QVariant(); +} diff --git a/MapModel.h b/MapModel.h new file mode 100644 index 0000000..a5d0fe2 --- /dev/null +++ b/MapModel.h @@ -0,0 +1,40 @@ +#ifndef MAPMODEL_H +#define MAPMODEL_H + +#include +#include + +/** + * @brief The MapModel class + * @author mhcuervo + * + * COPYRIGHT NOTICE: this class was originally written by mhcuervo as posted on + * http://stackoverflow.com/questions/23484511/how-to-display-a-simple-qmap-in-a-qtableview-in-qt + * Changes were made due to refactoring and adaption to the concrete use case. + */ +namespace q2d { +namespace util { + +class MapModel : public QAbstractTableModel +{ + Q_OBJECT +private: + const QMap* m_map; +public: + + enum MapRoles { + KeyRole = Qt::UserRole + 1, + ValueRole + }; + + explicit MapModel(QObject *parent = 0); + int rowCount(const QModelIndex& parent = QModelIndex()) const; + int columnCount(const QModelIndex& parent = QModelIndex()) const; + QVariant data(const QModelIndex& index, int role = Qt::DisplayRole) const; + inline void setMap(const QMap* map) { m_map = map; } +}; + +} +} + +#endif // MAPMODEL_H diff --git a/gui/MainWindow.cpp b/gui/MainWindow.cpp index bb0e8ea..36197e4 100644 --- a/gui/MainWindow.cpp +++ b/gui/MainWindow.cpp @@ -1,12 +1,12 @@ #include "MainWindow.h" #include "ui_MainWindow.h" -#include "Application.h" -#include "Document.h" -#include "metamodel/Category.h" -#include "ComponentFactory.h" -#include "Constants.h" -#include "gui/SchematicsTab.h" +#include "../Application.h" +#include "../Document.h" +#include "../metamodel/Category.h" +#include "../ComponentFactory.h" +#include "../Constants.h" +#include "SchematicsTab.h" #include #include @@ -23,11 +23,10 @@ MainWindow::MainWindow(ApplicationContext* parent) : QMainWindow(), m_ui(new Ui::MainWindow) { Q_CHECK_PTR(parent); - this->m_context = parent; - + m_context = parent; m_ui->setupUi(this); - - this->m_application = qobject_cast(Application::instance()); + m_application = qobject_cast(Application::instance()); + m_resultDialog = nullptr; } MainWindow::~MainWindow() {} @@ -317,3 +316,19 @@ MainWindow::on_btn_addCategory_clicked() { // add a new category emit this->signal_createCategory(name, parent); } + +void +MainWindow::slot_displayQuantorResult(QString textualRepresentation, const QMap* resultMapping){ + + qDebug() << "Show Quantor result dialog"; + // TODO extend the result dialog so the instance can be reused, + // instead of been created anew every time + if(m_resultDialog != nullptr){ + delete m_resultDialog; + m_resultDialog = nullptr; + } + m_resultDialog = new QuantorResultDialog(this, textualRepresentation, resultMapping); + m_resultDialog->show(); + m_resultDialog->raise(); + m_resultDialog->activateWindow(); +} diff --git a/gui/MainWindow.h b/gui/MainWindow.h index e851039..9642257 100644 --- a/gui/MainWindow.h +++ b/gui/MainWindow.h @@ -4,7 +4,7 @@ #define MAINWINDOW_H #include "ui_MainWindow.h" - +#include "QuantorResultDialog.h" #include "metamodel/Category.h" #include @@ -31,6 +31,8 @@ class MainWindow : public QMainWindow { q2d::Application* m_application; q2d::ApplicationContext* m_context; + QuantorResultDialog* m_resultDialog; + void addNewSchematicsTab(Document* relatedDocument); public: @@ -65,6 +67,7 @@ public slots: void slot_openDocumentTab(const QModelIndex index); void slot_openDocumentTab(Document* document); void slot_setComponentModel(QStandardItemModel* model); + void slot_displayQuantorResult(QString textualRepresentation, const QMap* resultMapping); private slots: // created by the Qt Designer diff --git a/gui/QuantorResult.ui b/gui/QuantorResult.ui deleted file mode 100644 index bbe9aec..0000000 --- a/gui/QuantorResult.ui +++ /dev/null @@ -1,85 +0,0 @@ - - - Dialog - - - - 0 - 0 - 400 - 300 - - - - Dialog - - - - - - - - Result: - - - - - - - (NONE) - - - - - - - - - - - - Qt::Horizontal - - - QDialogButtonBox::Cancel|QDialogButtonBox::Ok - - - - - - - - - buttonBox - accepted() - Dialog - accept() - - - 248 - 254 - - - 157 - 274 - - - - - buttonBox - rejected() - Dialog - reject() - - - 316 - 260 - - - 286 - 274 - - - - - diff --git a/gui/QuantorResultDialog.cpp b/gui/QuantorResultDialog.cpp new file mode 100644 index 0000000..c70f4b9 --- /dev/null +++ b/gui/QuantorResultDialog.cpp @@ -0,0 +1,23 @@ +#include "QuantorResultDialog.h" +#include "ui_QuantorResultDialog.h" + +#include "../MapModel.h" + +#include + +QuantorResultDialog::QuantorResultDialog(QWidget *parent, QString resultText, const QMap* resultMapping) : + QDialog(parent), + m_ui(new Ui::QuantorResultDialog) +{ + m_ui->setupUi(this); + m_ui->lbl_resultText->setText(resultText); + q2d::util::MapModel* model = new q2d::util::MapModel(this); + model->setMap(resultMapping); + m_ui->table_Assignments->setModel(model); +} + +QuantorResultDialog::~QuantorResultDialog() +{ + m_ui->table_Assignments->model()->deleteLater(); + delete m_ui; +} diff --git a/gui/QuantorResultDialog.h b/gui/QuantorResultDialog.h new file mode 100644 index 0000000..77eccef --- /dev/null +++ b/gui/QuantorResultDialog.h @@ -0,0 +1,20 @@ +#ifndef QUANTORRESULTDIALOG_H +#define QUANTORRESULTDIALOG_H + +#include + +namespace Ui { +class QuantorResultDialog; +} + +class QuantorResultDialog : public QDialog +{ + Q_OBJECT +private: + Ui::QuantorResultDialog *m_ui; +public: + explicit QuantorResultDialog(QWidget *parent, QString resultText, const QMap* resultMapping); + ~QuantorResultDialog(); +}; + +#endif // QUANTORRESULTDIALOG_H diff --git a/gui/QuantorResultDialog.ui b/gui/QuantorResultDialog.ui new file mode 100644 index 0000000..0a7d69c --- /dev/null +++ b/gui/QuantorResultDialog.ui @@ -0,0 +1,42 @@ + + + QuantorResultDialog + + + + 0 + 0 + 400 + 300 + + + + Dialog + + + + + + + + Result: + + + + + + + (NONE) + + + + + + + + + + + + + diff --git a/interfaces/Quantor.cpp b/interfaces/Quantor.cpp index f240e52..6834e55 100644 --- a/interfaces/Quantor.cpp +++ b/interfaces/Quantor.cpp @@ -35,21 +35,34 @@ QuantorInterface::buildContexts(q2d::model::Model const &contextSource, QIContext globalContext = QIContext(currentIndex); globalContext.addFunction(targetFunction); + // IMPORTANT: build the ports before the wires + // otherwise the generated context is wrong + for (model::Port * port : contextSource.outsidePorts()) { + if(port->direction() == model::enums::PortDirection::OUT){ + // this is a special case handling. more a hack then proper design + // TODO subclass port to handle properly + for(QString varName : port->nodeVariables()){ + globalContext.assignVariable(varName, VariableType::INPUT); + } + } else { + globalContext.addModelElement(*port); + } + } + for (model::ModelElement * wire : contextSource.conductors()) { globalContext.addModelElement(*wire); } - for (model::ModelElement * port : contextSource.outsidePorts()) { - globalContext.addModelElement(*port); - } currentIndex = globalContext.highestIndex() + 1; m_contexts.insert(GLOBAL_CONTEXT_NAME, globalContext); + globalContext.dumpMaps(); qDebug() << "Building component contexts"; for (model::ModelElement * c : contextSource.components()) { QIContext newContext = QIContext(currentIndex, c, &globalContext); currentIndex = newContext.highestIndex() + 1; m_contexts.insert(c->relatedEntry()->id(), newContext); + newContext.dumpMaps(); } } @@ -76,8 +89,6 @@ QuantorInterface::slot_solveProblem(Document* targetDocument, QString targetFunc Q_ASSERT(!(m_solution.isEmpty() && !rawSolution.empty())); // DEBUG - // FIXME known bug - // rawSolution is empty qDebug() << "Solutions:"; for(int i : m_solution){ qDebug() << util::intToString(i); @@ -103,6 +114,7 @@ QuantorInterface::interpreteSolution(const Result &result){ // resolve variable numbers to names and // translate sign to truth value + // TODO it is sufficient to onle ask for configVars. Others will not be included in the solution QMap* resultMapping = new QMap(); QMapIterator contextIter(m_contexts); @@ -121,8 +133,10 @@ QuantorInterface::interpreteSolution(const Result &result){ } } } + qDebug() << "Sending result and solution"; emit signal_hasSolution(textualResult, resultMapping); } else { - emit signal_hasSolution(textualResult); + qDebug() << "Sending result"; + emit signal_hasSolution(textualResult, nullptr); } } diff --git a/interfaces/Quantor.h b/interfaces/Quantor.h index 1e52d66..64ec313 100644 --- a/interfaces/Quantor.h +++ b/interfaces/Quantor.h @@ -63,7 +63,8 @@ public slots: * @param variableMapping provides a mapping from variable names to truth values if there was found one. * This may be null, if the result does not incorporate a variable assignment */ - void signal_hasSolution(QString textualRepresentation, const QMap* variableMapping = nullptr); + void signal_hasSolution(QString textualRepresentation, const QMap* variableMapping); + // TODO better wrap the parameters in a solution object. }; } // namespace quantor diff --git a/interfaces/quantor/QIContext.cpp b/interfaces/quantor/QIContext.cpp index ae92655..f4c20a8 100644 --- a/interfaces/quantor/QIContext.cpp +++ b/interfaces/quantor/QIContext.cpp @@ -6,7 +6,7 @@ // for debug purposes #include "../../DocumentEntry.h" - +#include #include "QtDebug" using namespace q2d::constants; @@ -139,3 +139,28 @@ QIContext::typeOf(std::string varName) const { return this->typeOf(var); } } + +void +QIContext::dumpMaps(){ + qDebug() << "=== Dumping Context ==="; + qDebug() << "variable assignments:"; + QMapIterator iterVar(m_variableMapping); + while(iterVar.hasNext()){ + iterVar.next(); + qDebug() << iterVar.key() << "->" << QString::number(iterVar.value()); + } + + qDebug() << "variable types:"; + QMapIterator iterType(m_typeMapping); + while(iterType.hasNext()){ + iterType.next(); + qDebug() << QString::number(iterType.key()) << "->" << QString::number((int)iterType.value()); + } + + qDebug() << "Functions:"; + for(std::string entry : m_functions){ + qDebug() << QString::fromStdString(entry); + } + + qDebug() << "=== End dump ==="; +} diff --git a/interfaces/quantor/QIContext.h b/interfaces/quantor/QIContext.h index 1e2ff16..5c66624 100644 --- a/interfaces/quantor/QIContext.h +++ b/interfaces/quantor/QIContext.h @@ -40,9 +40,13 @@ class QIContext { QMap m_typeMapping; QList m_functions; - void assignVariable(QString varName, VariableType type); + public: + // TODO should be private + // public due to hack + void assignVariable(QString varName, VariableType type); + /** * @brief QIContext creates a minimal, empty context to be filled manually. * @param contextName @@ -78,6 +82,11 @@ class QIContext { QList const &functions() const { return m_functions; } + + /** + * @brief dumpMaps is a helper function for debugging + */ + void dumpMaps(); }; } // namespace quantor diff --git a/interfaces/quantor/Quantorizer.cpp b/interfaces/quantor/Quantorizer.cpp index fb8f996..c7438c2 100644 --- a/interfaces/quantor/Quantorizer.cpp +++ b/interfaces/quantor/Quantorizer.cpp @@ -1,6 +1,7 @@ #line 68 "Quantorizer.ypp" #include "Quantorizer.hpp" +#include using namespace q2d::quantor; @@ -94,12 +95,13 @@ unsigned Quantorizer::nextToken(YYSVal &sval) { break; } if(res == 0) { - std::string name(formula, len); - unsigned const var = (*context)[name]; - assert(var <= max_named); - if(var == 0) error("Could not resolve variable \"" + name + '"'); - sval = var; - res = IDENT; + std::string name(formula, len); + qDebug() << "Resolving" << name.c_str(); + unsigned const var = (*context)[name]; + assert(var <= max_named); + if(var == 0) error("Could not resolve variable \"" + name + '"'); + sval = var; + res = IDENT; } formula = p; return res; @@ -113,6 +115,18 @@ unsigned Quantorizer::nextToken(YYSVal &sval) { //- Public Usage Interface --------------------------------------------------- inline Result Quantorizer::solve0(QICircuit const &c, std::vector &sol) { // Quantifier Preamble + + // DEBUG + for(unsigned i : c.configVars()){ + qDebug() << "Config var" << i; + } + for(unsigned i : c.inputVars()){ + qDebug() << "Input var" << i; + } + for(unsigned i : c.nodeVars()){ + qDebug() << "Node var" << i; + } + // END DEBUG openScope(QUANTOR_EXISTENTIAL_VARIABLE_TYPE, c.configVars()); closeScope(); openScope(QUANTOR_UNIVERSAL_VARIABLE_TYPE, c.inputVars()); @@ -134,7 +148,11 @@ inline Result Quantorizer::solve0(QICircuit const &c, std::vector &sol) { // Finish Problem Specification closeScope(); - for(int lit : clauses) quantor.add(lit); + QString debugText = "clauses: "; + for(int lit : clauses) { + debugText.append(QString::number(lit)).append(", "); + quantor.add(lit);} + qDebug() << debugText << ""; // Solve Problem Result const res = quantor.sat(); @@ -187,7 +205,7 @@ class q2d::quantor::Quantorizer::YYStack { unsigned short operator*() const { return stack.back().state; } }; -char const *const q2d::quantor::Quantorizer::yyterms[] = { "EOF", +char const *const q2d::quantor::Quantorizer::yyterms[] = { "EOF", "NOT", "AND", "OR", "XOR", "NAND", "NOR", "XNOR", "IDENT", "'='", "'('", "')'", }; unsigned short const q2d::quantor::Quantorizer::yyintern[] = { @@ -344,7 +362,7 @@ void q2d::quantor::Quantorizer::parse() { YYSVal yylval; unsigned short const yyrno = (yyact < 0)? -yyact : 0; unsigned short const yylen = yylength[yyrno]; - + #ifdef TRACE std::cerr << "Reduce by " << yyrules[yyrno] << std::endl; #endif @@ -354,8 +372,8 @@ void q2d::quantor::Quantorizer::parse() { case 1: { #line 227 "Quantorizer.ypp" - addClause(yystack[yylen - 1]); - + addClause(yystack[yylen - 1]); + #line 359 "Quantorizer.cpp" break; } @@ -364,7 +382,7 @@ case 2: { addClause( yystack[yylen - 1], -yystack[yylen - 3]); addClause(-yystack[yylen - 1], yystack[yylen - 3]); - + #line 368 "Quantorizer.cpp" break; } @@ -376,7 +394,7 @@ case 3: { addClause(-res, yystack[yylen - 1]); addClause(-res, yystack[yylen - 3]); yylval = res; - + #line 380 "Quantorizer.cpp" break; } @@ -388,7 +406,7 @@ case 4: { addClause( res, -yystack[yylen - 1]); addClause( res, -yystack[yylen - 3]); yylval = res; - + #line 392 "Quantorizer.cpp" break; } @@ -401,7 +419,7 @@ case 5: { addClause( res, -yystack[yylen - 1], yystack[yylen - 3]); addClause( res, yystack[yylen - 1], -yystack[yylen - 3]); yylval = res; - + #line 405 "Quantorizer.cpp" break; } @@ -413,7 +431,7 @@ case 6: { addClause( res, yystack[yylen - 1]); addClause( res, yystack[yylen - 3]); yylval = res; - + #line 417 "Quantorizer.cpp" break; } @@ -425,7 +443,7 @@ case 7: { addClause(-res, -yystack[yylen - 1]); addClause(-res, -yystack[yylen - 3]); yylval = res; - + #line 429 "Quantorizer.cpp" break; } @@ -438,25 +456,25 @@ case 8: { addClause(-res, -yystack[yylen - 1], yystack[yylen - 3]); addClause(-res, yystack[yylen - 1], -yystack[yylen - 3]); yylval = res; - + #line 442 "Quantorizer.cpp" break; } case 9: { #line 278 "Quantorizer.ypp" - yylval = yystack[yylen - 1]; + yylval = yystack[yylen - 1]; #line 448 "Quantorizer.cpp" break; } case 10: { #line 279 "Quantorizer.ypp" - yylval = yystack[yylen - 1]; + yylval = yystack[yylen - 1]; #line 454 "Quantorizer.cpp" break; } case 11: { #line 280 "Quantorizer.ypp" - yylval = yystack[yylen - 2]; + yylval = yystack[yylen - 2]; #line 460 "Quantorizer.cpp" break; } @@ -467,12 +485,12 @@ case 12: { addClause( res, yystack[yylen - 2]); addClause(-res, -yystack[yylen - 2]); yylval = res; - + #line 471 "Quantorizer.cpp" break; } } - + yystack.pop(yylen); yystack.push(yygoto[*yystack][yylhs[yyrno]], yylval); } diff --git a/q2d.pro b/q2d.pro index a0eba53..68d7165 100644 --- a/q2d.pro +++ b/q2d.pro @@ -76,7 +76,9 @@ SOURCES +=\ $$picosatDir/picosat.c \ $$picosatDir/version.c \ #including relevant quantor files - $$quantorDir/quantor.c + $$quantorDir/quantor.c \ + gui/QuantorResultDialog.cpp \ + MapModel.cpp HEADERS +=\ gui/MainWindow.h \ @@ -122,7 +124,9 @@ HEADERS +=\ interfaces/quantor/VariableType.h \ interfaces/quantor/Result.h \ $$picosatDir/*.h \ - $$quantorDir/*.h + $$quantorDir/*.h \ + gui/QuantorResultDialog.h \ + MapModel.h INCLUDEPATH +=\ $$picosatDir \ @@ -131,7 +135,7 @@ INCLUDEPATH +=\ FORMS +=\ gui/MainWindow.ui \ gui/SchematicsTab.ui \ - gui/QuantorResult.ui + gui/QuantorResultDialog.ui # exclude quantorizer.ypp HEADERS -= interfaces/quantor/Quantorizer.ypp